Abstract
Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic timed automata which have one or two clocks. Firstly, we show that Pctl probabilistic model-checking problems (such as determining whether a set of target states can be reached with probability at least 0.99 regardless of how nondeterminism is resolved) are PTIME-complete for one clock probabilistic timed automata, and are EXPTIME-complete for probabilistic timed automata with two clocks. Secondly, we show that the model-checking problem for the probabilistic timed temporal logic Ptctl is EXPTIME-complete for one clock probabilistic timed automata. However, the corresponding model-checking problem for the subclass of Ptctl which does not permit both (1) punctual timing bounds, which require the occurrence of an event at an exact time point, and (2) comparisons with probability bounds other than 0 or 1, is PTIME-complete.
Supported in part by EPSRC project EP/E022030/1, Miur project Firb-Perf, and EEC project Crutial.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., et al.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., et al. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005)
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 115–136. Springer, Heidelberg (1991)
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. and Comp. 104(1), 2–34 (1993)
Alur, R., Dill, D.L.: A theory of timed automata. Theo. Comp. Sci. 126(2), 183–235 (1994)
Baier, C., et al.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Soft. Enginee. 29(6), 524–541 (2003)
Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing 11(3), 125–155 (1998)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
de Alfaro, L.: Formal verification of probabilistic systems. PhD thesis, Stanford University, Department of Computer Science (1997)
de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 165–176. Springer, Heidelberg (1997)
Hansson, H.A., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Jensen, H.E.: Model checking probabilistic real time systems. In: Proc. of the 7th Nordic Work. on Progr. Theory, pp. 247–261. Chalmers Institute of Technology (1996)
Kwiatkowska, M., et al.: Performance analysis of probabilistic timed automata using digital clocks. Formal Meth. in Syst. Design 29, 33–78 (2006)
Kwiatkowska, M., et al.: Automatic verification of real-time systems with discrete probability distributions. Theo. Comp. Sci. 286, 101–150 (2002)
Laroussinie, F., Markey, N., Oreiby, G.: Model checking timed ATL for durational concurrent game structures. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 245–259. Springer, Heidelberg (2006)
Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004)
Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theo. Comp. Sci. 353(1–3), 249–271 (2005)
Laroussinie, F., Sproston, J.: Model checking durational probabilistic systems. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 140–154. Springer, Heidelberg (2005)
Laroussinie, F., Sproston, J.: State explosion in almost-sure probabilistic reachability. To appear in IPL (2007)
Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 299–314. Springer, Heidelberg (2005)
Papadimitriou, C., Tsitsiklis, J.: The complexity of Markov decision processes. Mathematics of Operations Research 12(3), 441–450 (1987)
Stoelinga, M.: Alea Jacta est: Verification of probabilistic, real-time and parametric systems. PhD thesis, Institute for Computing and Information Sciences, University of Nijmegen (2002)
Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed Büchi automata emptiness efficiently. Formal Meth. in Syst. Design 26(3), 267–292 (2005)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of the 16th An. Symp. on Foundations of Computer Science (FOCS’85), pp. 327–338. IEEE Computer Society Press, Los Alamitos (1985)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Jurdziński, M., Laroussinie, F., Sproston, J. (2007). Model Checking Probabilistic Timed Automata with One or Two Clocks. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)