Abstract
Continuous Time Markov Chains (CTMCs) are widely used as the underlying stochastic process in performance and dependability analysis. Model checking of CTMCs against Continuous Stochastic Logic (CSL) has been investigated previously by a number of authors [2,4,13]. CSL contains a time-bounded until operator that allows one to express properties such as “the probability of 3 servers becoming faulty within 7.01 seconds is at most 0.1”. In this paper we extend CSL with a random time-bounded until operator, where the time bound is given by a random variable instead of a fixed real-valued time (or interval). With the help of such an operator we can state that the probability of reaching a set of goal states within some generally distributed delay while passing only through states that satisfy a certain property is at most (at least) some probability threshold. In addition, certain transient properties of systems which contain general distributions can be expressed with the extended logic. We extend the efficient model checking of CTMCs against the logic CSL developed in [13] to cater for the new operator. Our method involves precomputing a family of coefficients for a range of random variables which includes Pareto, uniform and gamma distributions, but otherwise carries the same computational cost as that for ordinary time-bounded until in [13]. We implement the algorithms in Matlab and evaluate them by means of a queueing system example.
Partly supported by EPSRC grant GR/M13046, FCT, grant SFRH/BSAB/251/01 and the projects POSI/34826/CPS/2000 and POSI/42069/CPS/2001.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In Proc. CAV’96, volume 1102 of LNCS, pages 269–276. Springer, 1996.
A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model checking continuous time Markov chains. ACM Transactions on Computational Logic, 1(1):162–170, 2000.
C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Proc. CAV 2000, volume 1855 of LNCS, pages 358–372, 2000.
C. Baier, J.-P. Katoen, and H. Hermanns. Approximative symbolic model checking of continuous-time Markov chains. In Proc. CONCUR’99, volume 1664 of LNCS, pages 146–162. Springer, 1999.
E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
M. Crovella and A. Bestavros. Self-similarity in world wide Web traffic: evidence and possible causes. IEEE/ACM Transactions on Networking, 5(6):835–846, 1997.
B. Fox and P. Glynn. Computing Poisson probabilities. Communications of the ACM, 31(4):440–445, 1988.
R. German. Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley and Sons, 2000.
J. Grandell. Mixed Poisson Processes. Chapman & Hall, 1997.
D. Gross and D. Miller. The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research, 32(2):343–361, 1984.
H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6:512–535, 1994.
A. Jensen. Markov chains as an aid in the study of Markov processes. Skandinavisk Aktuarietidsskrift, Marts, pages 87–91, 1953.
J.-P. Katoen, M. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic CTMC model checking. In Proc. PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 23–38. Springer, 2001.
M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In Proc. TACAS 2002, volume 2280 of LNCS, pages 52–66. Springer, 2002.
G.I. Lópes, H. Hermanns, and J.-P. Katoen. Beyond memoryless distributions. In Proc PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 57–70. Springer, 2001.
S. Molnár and I. Maricza, editors. Source characterization in broadband networks. COST 257 Mid-term seminar interim report on source characterization, 2000.
J. Muppala and K. Trivedi. Queueing Systems, Queueing and Related Models, chapter Numerical Transient Solution of Finite Markovian Queueing Systems, pages 262–284. Oxford University Press, 1992.
H. Panjer. Recursive evaluation of a family of compound distributions. Astin Bulletin, 12(1):22–26, 1982.
PRISM web page. http://www.cs.bham.ac.uk/~dxp/prism/.
W. J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kwiatkowska, M., Norman, G., Pacheco, A. (2002). Model Checking CSL until Formulae with Random Time Bounds. In: Hermanns, H., Segala, R. (eds) Process Algebra and Probabilistic Methods: Performance Modeling and Verification. PAPM-PROBMIV 2002. Lecture Notes in Computer Science, vol 2399. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45605-8_10
Download citation
DOI: https://doi.org/10.1007/3-540-45605-8_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43913-4
Online ISBN: 978-3-540-45605-6
eBook Packages: Springer Book Archive