×

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:

Uppaal2k; PRISM; Kronos
PDFBibTeX XMLCite
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
[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, (Hermanns, H.; Segala, R., Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV’02). Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV’02), Lecture Notes in Computer Science, vol. 2399 (2002), Springer-Verlag), 169-187 · Zbl 1065.68583
[10] Kwiatkowska, M.; Norman, G.; Parker, D.; Sproston, J., Performance analysis of probabilistic timed automata using digital clocks, (Larsen, K.; Niebert, P., Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS’03). Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS’03), LNCS, vol. 2791 (2003), Springer-Verlag), 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., Uppaal—present and future, (Proceedings of the 40th IEEE Conference on Decision and Control (CDC’01), vol. 3 (2001), IEEE Computer Society Press), 2881-2886
[14] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S., The tool Kronos, (Alur, R.; Henzinger, T.; Sontag, E., Hybrid Systems III: Verification and Control. Hybrid Systems III: Verification and Control, Lecture Notes in Computer Science, vol. 1066 (1996), Springer-Verlag), 208-219
[15] Daws, C.; Kwiatkowska, M.; Norman, G., Automatic verification of the IEEE 1394 root contention protocol with Kronos and PRISM, International Journal on Software Tools for Technology Transfer (STTT), 5, 2-3, 221-236 (2004)
[17] Bianco, A.; de Alfaro, L., Model checking of probabilistic and nondeterministic systems, (Thiagarajan, P., Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’95). Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’95), Lecture Notes in Computer Science, vol. 1026 (1995), Springer-Verlag), 499-513 · Zbl 1354.68167
[18] Dill, D., Timing assumptions and verification of finite-state concurrent system, (Sifakis, J., Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems. Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol. 407 (1989), Springer-Verlag), 197-212
[21] Kwiatkowska, M.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, (Lakhnech, Y.; Yovine, S., Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT). Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), Lecture Notes in Computer Science, vol. 3253 (2004), Springer-Verlag), 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: 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) · Zbl 1448.68285
[25] Manna, Z.; Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems: Specification (1992), Springer Verlag: Springer Verlag New York
[27] Dill, D., Timing assumptions and verification of finite-state concurrent systems, (Sifakis, J., Proceedings of the Automatic Verification Methods for Finite State Systems. Proceedings of the Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol. 407 (1989), Springer-Verlag), 197-212
[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
[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, (Proceedings of the 15th Annual ACM Symposium on Theory of Computing (STOC’83) (1983), ACM Press), 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, (Graf, S.; Schwartzbach, M., Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00). Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), LNCS, vol. 1785 (2000), Springer), 395-410 · Zbl 0960.68109
[35] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM: probabilistic symbolic model checker, (Field, T.; Harrison, P.; Bradley, J.; Harder, U., Proceedings of TOOLS’02. Proceedings of TOOLS’02, Lecture Notes in Computer Science, vol. 2324 (2002), Springer-Verlag), 200-204 · Zbl 1047.68533
[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, (Ibarra, O. H.; Dang, Z., Proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA’03). Proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA’03), Lecture Notes in Computer Science, vol. 2759 (2003), Springer-Verlag), 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, (Cleaveland, R., Proceedings of the 3rd International Conference on Concurrency Theory (CONCUR’92). Proceedings of the 3rd International Conference on Concurrency Theory (CONCUR’92), Lecture Notes in Computer Science, vol. 630 (1992), Springer-Verlag), 340-354
[43] Kwiatkowska, M.; Norman, G.; Sproston, J., Symbolic computation of maximal probabilistic reachability, (Larsen, K.; Nielsen, M., Proceedings of the 13th International Conference on Concurrency Theory (CONCUR’01). Proceedings of the 13th International Conference on Concurrency Theory (CONCUR’01), Lecture Notes in Computer Science, vol. 2154 (2001), Springer-Verlag), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.