×

Stochastic games for verification of probabilistic timed automata. (English) Zbl 1262.68125

Ouaknine, Joël (ed.) et al., Formal modeling and analysis of timed systems. 7th international conference, FORMATS 2009, Budapest, Hungary, September 14–16, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04367-3/pbk). Lecture Notes in Computer Science 5813, 212-227 (2009).
Summary: Probabilistic timed automata (PTAs) are used for formal modelling and verification of systems with probabilistic, nondeterministic and real-time behaviour. For non-probabilistic timed automata, forwards reachability is the analysis method of choice, since it can be implemented extremely efficiently. However, for PTAs, such techniques are only able to compute upper bounds on maximum reachability probabilities. In this paper, we propose a new approach to the analysis of PTAs using abstraction and stochastic games. We show how efficient forwards reachability techniques can be extended to yield both lower and upper bounds on maximum (and minimum) reachability probabilities. We also present abstraction-refinement techniques that are guaranteed to improve the precision of these probability bounds, providing a fully automatic method for computing the exact values. We have implemented these techniques and applied them to a set of large case studies. We show that, in comparison to alternative approaches to verifying PTAs, such as backwards reachability and digital clocks, our techniques exhibit superior performance and scalability.
For the entire collection see [Zbl 1176.68014].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
91A15 Stochastic games, stochastic differential games
91A80 Applications of game theory

Software:

Uppaal; Kronos
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Beauquier, D.: Probabilistic timed automata. Theoretical Computer Science 292(1), 65–84 (2003) · Zbl 1064.68063 · doi:10.1016/S0304-3975(01)00215-8
[2] Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003) · doi:10.1007/3-540-36494-3_54
[3] Chen, T., Han, T., Katoen, J.-P.: Time-abstracting bisimulation for probabilistic timed automata. In: Proc. TASE 2008, pp. 177–184. IEEE CS Press, Los Alamitos (2008)
[4] Condon, A.: The complexity of stochastic games. Inf. and Comp. 96(2), 203–224 (1992) · Zbl 0756.90103 · doi:10.1016/0890-5401(92)90048-K
[5] 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) · Zbl 02243217 · doi:10.1007/s10009-003-0118-5
[6] Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996) · doi:10.1007/BFb0020947
[7] Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007) · Zbl 1141.68431 · doi:10.1007/978-3-540-75454-1_10
[8] Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. and Comp. 111(2), 193–244 (1994) · Zbl 0806.68080 · doi:10.1006/inco.1994.1045
[9] Jensen, H.: Model checking probabilistic real time systems. In: Proc. 7th Nordic Workshop on Programming Theory, pp. 247–261 (1996)
[10] Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Technical Report RR-08-06, Oxford University Computing Laboratory (February 2008) · Zbl 1233.90276
[11] Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 182–197. Springer, Heidelberg (2009) · Zbl 1206.68090 · doi:10.1007/978-3-540-93900-9_17
[12] Kemper, S., Platzer, A.: SAT-based abstraction refinement for real-time systems. In: Proc. FACS 2006. ENTCS, vol. 182, pp. 107–122 (2007) · doi:10.1016/j.entcs.2006.09.034
[13] Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST 2006, pp. 157–166. IEEE CS Press, Los Alamitos (2006)
[14] Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. Technical Report RR-09-05, Oxford University Computing Laboratory (2009) · Zbl 1262.68125
[15] Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design 29, 33–78 (2006) · Zbl 1105.68063 · doi:10.1007/s10703-006-0005-2
[16] 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 · doi:10.1016/S0304-3975(01)00046-9
[17] Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. and Comp. 205(7), 1027–1077 (2007) · Zbl 1122.68075 · doi:10.1016/j.ic.2007.01.004
[18] Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997) · Zbl 1060.68577 · doi:10.1007/s100090050010
[19] Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994) · Zbl 0829.90134 · doi:10.1002/9780470316887
[20] Shapley, L.: Stochastic games. Proc. National Academy of Science 39, 1095–1100 (1953) · Zbl 0051.35805 · doi:10.1073/pnas.39.10.1095
[21] Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004) · Zbl 1109.68507 · doi:10.1007/978-3-540-30206-3_25
[22] Tripakis, S.: The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourier (1998)
[23] Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999) · doi:10.1007/3-540-48778-6_18
[24] Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed Büchi automata emptiness efficiently. Formal Methods in System Design 26(3), 267–292 (2005) · Zbl 1085.68083 · doi:10.1007/s10703-005-1632-8
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.