Abstract
We consider model-checking algorithms for durational probabilistic systems, which are systems exhibiting nondeterministic, probabilistic and discrete-timed behaviour. We present two semantics for durational probabilistic systems, and show how formulae of the probabilistic and timed temporal logic Ptctl can be verified on such systems. We also address complexity issues, in particular identifying the cases in which model checking durational probabilistic systems is harder than verifying non-probabilistic durational systems.
Supported in part by MIUR-FIRB Perf.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 104(1), 2–34 (1993)
Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Heidelberg (2004)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 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)
Campos, S., Clarke, E.M., Marrero, W.R., Minea, M., Hiraishi, H.: Computing quantitative characteristic of finite-state real-time systems. In: Proc. IEEE Real-Time Systems Symposium (RTSS 1994), pp. 266–270. IEEE Computer Society Press, Los Alamitos (1994)
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)
Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real Time Systems 4(4), 331–352 (1992)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, New York (1979)
Hansson, H.A., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Kwiatkowska, M.: Model checking for probability and time: From theory to practice. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 351–360. IEEE Computer Society Press, Los Alamitos (2003)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 286, 101–150 (2002)
Laroussinie, F., Markey, N., Schnoebelen, P.: On model checking durational Kripke structures (extended abstract). In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 264–279. Springer, Heidelberg (2002)
Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete time systems (2004) (submitted)
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)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 16th Annual Symp. on Foundations of Computer Science (FOCS 1985), pp. 327–338. IEEE Computer Society Press, Los Alamitos (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laroussinie, F., Sproston, J. (2005). Model Checking Durational Probabilistic Systems. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)