Abstract
We give a sufficient condition under which every finite-satisfiable formula of a given PCTL fragment has a model with at most doubly exponential number of states (consequently, the finite satisfiability problem for the fragment is in \(\mathbf{2}\text {-}{} \mathbf{EXPSPACE}\)). The condition is semantic and it is based on enforcing a form of “progress” in non-bottom SCCs contributing to the satisfaction of a given PCTL formula. We show that the condition is satisfied by PCTL fragments beyond the reach of existing methods.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Although there are uncountably many Markov chains with n states, the edge probabilities can be represented symbolically by variables, and the satisfiability of a given PCTL formula in a Markov chain with n states can then be encoded in the existential fragment of first-order theory of the reals. This construction is presented in [13].
- 2.
In [22], the formula \(\psi \) has the same structure but uses qualitative probability constraints.
- 3.
We do not include formulae with the trivial “\({\ge } 0\)” probability constraint.
References
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998)
Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62–74. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51803-7_22
Bertrand, N., Fearnley, J., Schewe, S.: Bounded satisfiability for PCTL. In: Proceedings of CSL 2012. Leibniz International Proceedings in Informatics, vol. 16, pp. 92–106. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2012)
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). https://doi.org/10.1007/3-540-60692-0_70
Billingsley, P.: Probability and Measure. Wiley, Hoboken (1995)
Brázdil, T., Brožek, V., Forejt, V., Kučera, A.: Stochastic games with branching-time winning objectives. In: Proceedings of LICS 2006, pp. 349–358. IEEE Computer Society Press (2006)
Brázdil, T., Forejt, V., Křetínský, J., Kučera, A.: The satisfiability problem for probabilistic CTL. In: Proceedings of LICS 2008, pp. 391–402. IEEE Computer Society Press (2008)
Brázdil, T., Forejt, V., Křetínský, J., Kučera, A.: The satisfiability problem for probabilistic CTL. Technical report FIMU-RS-2008-03, Faculty of Informatics, Masaryk University (2008)
Brázdil, T., Forejt, V., Kučera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 148–159. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_13
Brázdil, T., Kučera, A., Stražovský, O.: On the decidability of temporal properties of probabilistic pushdown automata. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 145–157. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31856-9_12
Chakraborty, S., Katoen, J.: On the satisfiability of some simple probabilistic logics. In: Proceedings of LICS 2016, pp. 56–65 (2016)
Chodil, M., Kučera, A.: The satisfiability problem for a quantitative fragment of PCTL. arXiv:2107.03794 [cs.LO] (2021)
Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science B, pp. 995–1072 (1991)
Emerson, E., Halpern, J.: Decision procedures and expressiveness in the temporal logic of branching time. In: Proceedings of STOC 1982, pp. 169–180. ACM Press (1982)
Esparza, J., Kučera, A., Mayr, R.: Model-checking probabilistic pushdown automata. Logical Methods Comput. Sci. 2(1:2), 1–31 (2006)
Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Logic 13 (2012)
Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6, 512–535 (1994)
Hart, S., Sharir, M.: Probabilistic temporal logic for finite and bounded models. In: Proceedings of POPL 1984, pp. 1–13. ACM Press (1984)
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proceedings of LICS 1997, pp. 111–122. IEEE Computer Society Press (1997)
Křetínský, J., Rotar, A.: The satisfiability problem for unbounded fragments of probabilistic CTL. In: Proceedings of CONCUR 2018. Leibniz International Proceedings in Informatics, vol. 118, pp. 32:1–32:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2018)
Lehman, D., Shelah, S.: Reasoning with time and chance. Inf. Control 53, 165–198 (1982)
Acknowledgement
The work is supported by the Czech Science Foundation, Grant No. 21-24711S.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Chodil, M., Kučera, A. (2021). The Satisfiability Problem for a Quantitative Fragment of PCTL. In: Bampis, E., Pagourtzis, A. (eds) Fundamentals of Computation Theory. FCT 2021. Lecture Notes in Computer Science(), vol 12867. Springer, Cham. https://doi.org/10.1007/978-3-030-86593-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-86593-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-86592-4
Online ISBN: 978-3-030-86593-1
eBook Packages: Computer ScienceComputer Science (R0)