×

zbMATH — the first resource for mathematics

Symbolic model checking for probabilistic timed automata. (English) Zbl 1122.68075
Summary: Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Software:
Kronos; PRISM; Uppaal2k
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (1999), MIT Press
[2] Burch, J.; Clarke, E.; McMillan, K.; Dill, D.; Hwang, L., Symbolic model checking: 10^20 states and beyond, Information and computation, 98, 2, 142-170, (1992) · Zbl 0753.68066
[3] Kwiatkowska, M.; Norman, G.; Segala, R.; Sproston, J., Automatic verification of real-time systems with discrete probability distributions, Theoretical computer science, 282, 101-150, (2002) · Zbl 1050.68094
[4] H. Jensen, Model checking probabilistic real time systems, in: B. Bjerner, M. Larsson, B. Nordström, (Eds.), Proceedings of the 7th Nordic Workshop on Programming Theory, Report 86, Chalmers University of Technology, 1996, pp. 247-261.
[5] Beauquier, D., Probabilistic timed automata, Theoretical computer science, 292, 1, 65-84, (2003) · Zbl 1064.68063
[6] Alur, R.; Dill, D., A theory of timed automata, Theoretical computer science, 126, 2, 183-235, (1994) · Zbl 0803.68071
[7] Henzinger, T.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Information and computation, 111, 2, 193-244, (1994) · Zbl 0806.68080
[8] Kwiatkowska, M.; Norman, G.; Sproston, J., Probabilistic model checking of deadline properties in the IEEE 1394 firewire root contention protocol, Formal aspects of computing, 14, 295-318, (2003) · Zbl 1029.68017
[9] Kwiatkowska, M.; Norman, G.; Sproston, J., Probabilistic model checking of the IEEE 802.11 wireless local area network protocol, (), 169-187 · Zbl 1065.68583
[10] Kwiatkowska, M.; Norman, G.; Parker, D.; Sproston, J., Performance analysis of probabilistic timed automata using digital clocks, (), 105-120 · Zbl 1099.68534
[11] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal aspects of computing, 6, 4, 512-535, (1994) · Zbl 0820.68113
[12] Alur, R.; Courcoubetis, C.; Dill, D., Model checking in dense real time, Information and computation, 104, 1, 2-34, (1993) · Zbl 0783.68076
[13] Behrmann, G.; David, A.; Larsen, K.; Möller, O.; Pettersson, P.; Yi, W., U\scppaal—present and future, (), 2881-2886
[14] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S., The tool K\scronos, (), 208-219
[15] Daws, C.; Kwiatkowska, M.; Norman, G., Automatic verification of the IEEE 1394 root contention protocol with K\scronos and PRISM, International journal on software tools for technology transfer (STTT), 5, 2-3, 221-236, (2004)
[16] L. de Alfaro, Formal Verification of Probabilistic Systems, Ph.D. thesis, Stanford University, 1997.
[17] Bianco, A.; de Alfaro, L., Model checking of probabilistic and nondeterministic systems, (), 499-513 · Zbl 1354.68167
[18] Dill, D., Timing assumptions and verification of finite-state concurrent system, (), 197-212
[19] IEEE 802.3-2002. Carrier Sense Multiple Access with Collision Detection (CSMA/CD) Standard, 2002.
[20] IEEE 1394-1995. High Performance Serial Bus Standard, 1995.
[21] Kwiatkowska, M.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, (), 293-308 · Zbl 1109.68517
[22] Kemeny, J.; Snell, J.; Knapp, A., Denumerable Markov chains, (1976), Springer-Verlag · Zbl 0348.60090
[23] Derman, C., Finite-state Markovian decision processes, (1970), Academic Press New York · Zbl 0262.90001
[24] Baier, C.; Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness, Distributed computing, 11, 3, 125-155, (1998)
[25] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems: specification, (1992), Springer Verlag New York
[26] R. Segala, Modelling and verification of randomized distributed real time systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995.
[27] Dill, D., Timing assumptions and verification of finite-state concurrent systems, (), 197-212
[28] S. Tripakis, L’analyse formelle des systèmes temporisés en pratique, Ph.D. thesis, Université Joseph Fourier, 1998.
[29] Clarke, E.; Emerson, E.; Sistla, A., Automatic verification of finite-state concurrent systems using temporal logics, ACM transactions on programming languages and systems, 8, 2, 244-263, (1986) · Zbl 0591.68027
[30] C. Baier, On algorithmic verification methods for probabilistic systems, habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim, 1998.
[31] Hart, S.; Sharir, M.; Pnueli, A., Termination of probabilistic concurrent programs, ACM transactions on programming languages and systems, 5, 3, 356-380, (1983) · Zbl 0511.68009
[32] Pnueli, A., On the extremely fair treatment of probabilistic algorithms, (), 278-290
[33] de Alfaro, L.; Kwiatkowska, M.; Norman, G.; Parker, D.; Segala, R., Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation, (), 395-410 · Zbl 0960.68109
[34] PRISM Web site, Available from: <www.cs.bham.ac.uk/ dxp/prism/>.
[35] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM: probabilistic symbolic model checker, (), 200-204 · Zbl 1047.68533
[36] S. Yovine, Méthodes et outils pour la vérification symbolique de systemés temporisés, Ph.D. thesis, Institut National Polytechnique de Grenoble, 1993.
[37] A. Olivero, Modélisation et analyse de systémes temporisés et hybrides, Ph.D. thesis, Institut National Polytechnique de Grenoble, 1994.
[38] C. Daws, Private communication, 2004.
[39] Nicollin, X.; Sifakis, J.; Yovine, S., Compiling real-time specifications into extended automata, IEEE transactions on software engineering, 18, 9, 794-804, (1992)
[40] Wang, F.; Hwang, G.; Yu, F., TCTL inevitability analysis of dense-time systems, (), 176-187 · Zbl 1279.68223
[41] Simons, D.; Stoelinga, M., Mechanical verification of the IEEE 1394a root contention protocol using uppaal2k, Springer international journal of software tools for technology transfer (STTT), 3, 4, 469-485, (2001) · Zbl 1053.68580
[42] Alur, R.; Courcoubetis, C.; Dill, D.; Halbwachs, N.; Wong-Toi, H., Minimization of timed transition systems, (), 340-354
[43] Kwiatkowska, M.; Norman, G.; Sproston, J., Symbolic computation of maximal probabilistic reachability, (), 169-183 · Zbl 1006.68096
[44] Henzinger, T.; Majumdar, R.; Raskin, J.-F., A classification of symbolic transition systems, ACM transactions on computational logic, 6, 1, 1-32, (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.