Document Open Access Logo

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL

Authors Jan Kretínský , Alexej Rotar

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.32.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Jan Kretínský
  • Technical University of Munich, Germany
Alexej Rotar
  • Technical University of Munich, Germany

Funding

This research was funded in part by the Czech Science Foundation grant No. P202/12/G061, TUM IGSSE Grant 10.06 (PARSEC), and the German Research Foundation (DFG) project 383882557 "Statistical Unbounded Verification".

Cite AsGet BibTex

Jan Kretínský and Alexej Rotar. The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.32

Abstract

We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establish decidability for several fragments containing quantitative operators and pinpoint the difficulties arising in more complex fragments where the decidability remains open.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • temporal logic
  • probabilistic verification
  • probabilistic computation tree logic
  • satisfiability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. C. Baier, M. Größer, M. Leucker, B. Bollig, and F. Ciesinski. Controller synthesis for probabilistic systems. In Proceedings of IFIP TCS'2004, pages 493-506. Kluwer, 2004. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008. Google Scholar
  3. B. Banieqbal and H. Barringer. Temporal logic with fixed points. In Temporal Logic in Specification, volume 398 of LNCS, pages 62-74. Springer, 1987. Google Scholar
  4. Nathalie Bertrand, John Fearnley, and Sven Schewe. Bounded satisfiability for PCTL. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, pages 92-106, 2012. Google Scholar
  5. T. Brázdil, V. Brožek, V. Forejt, and A. Kučera. Stochastic games with branching-time winning objectives. In Proceedings of LICS 2006, pages 349-358. IEEE, 2006. Google Scholar
  6. T. Brázdil, V. Forejt, and A. Kučera. Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. In Proceedings of ICALP 2008, LNCS. Springer, 2008. Google Scholar
  7. T. Brázdil, V. Forejt, J. Křetínský, and A. Kučera. The satisfiability problem for probabilistic CTL. In LICS, pages 391-402. IEEE, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.21.
  8. T. Brázdil, A. Kučera, and O. Stražovský. On the decidability of temporal properties of probabilistic pushdown automata. In Diekert and Durand [11], pages 145-157. Google Scholar
  9. Souymodip Chakraborty and Joost-Pieter Katoen. On the satisfiability of some simple probabilistic logics. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 56-65. ACM, 2016. Google Scholar
  10. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. JACM, 42(4):857-907, 1995. Google Scholar
  11. Volker Diekert and Bruno Durand, editors. STACS 2005, 22nd Annual Symposium on Theoretical Aspects of Computer Science, Stuttgart, Germany, February 24-26, 2005, Proceedings, volume 3404 of Lecture Notes in Computer Science. Springer, 2005. Google Scholar
  12. E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. In Proceedings of STOC'82, pages 169-180. ACM, 1982. Google Scholar
  13. J. Esparza, A. Kučera, and R. Mayr. Model-checking probabilistic pushdown automata. Logical Methods in Computer Science, 2, 2006. URL: http://dx.doi.org/10.2168/LMCS-2(1:2)2006.
  14. K. Etessami and M. Yannakakis. Recursive Markov chains, stochastic grammars, and monotone systems of non-linear equations. In Diekert and Durand [11], pages 340-352. Google Scholar
  15. M. Fischer and R. Ladner. Propositional dynamic logic of regular programs. JCSS, 18:194-211, 1979. Google Scholar
  16. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. FAC, 6:512-535, 1994. Google Scholar
  17. S. Hart and M. Sharir. Probabilistic propositional temporal logics. Information and Control, 70(2/3):97-155, 1986. Google Scholar
  18. T. Henzinger, O. Kupferman, and R. Majumdar. On the universal and existential fragments of the μ-calculus. TCS, 354(2):173-186, 2006. Google Scholar
  19. M. Huth and M.Z. Kwiatkowska. Quantitative analysis and model checking. In Proceedings of LICS'97, pages 111-122. IEEE, 1997. Google Scholar
  20. D. Kozen. A finite-model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, 1988. Google Scholar
  21. S. Kraus and D. J. Lehmann. Decision procedures for time and chance (extended abstract). In FOCS, pages 202-209. IEEE, 1983. Google Scholar
  22. A. Kučera and O. Stražovský. On the controller synthesis for finite-state Markov decision processes. In Proceedings of FST&TCS 2005, volume 3821 of LNCS, pages 541-552. Springer, 2005. Google Scholar
  23. O. Kupferman and M.Y. Vardi. An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages and Systems (TOPLAS), 22:87-128, 2000. Google Scholar
  24. Jan Křetínský and Alexej Rotar. The satisfiability problem for unbounded fragments of probabilistic CTL. Technical report, arXiv.org, 2018. URL: http://arxiv.org/abs/1806.11418.
  25. D. J. Lehmann and S. Shelah. Reasoning with time and chance (extended abstract). In ICALP, volume 154 of LNCS, pages 445-457. Springer, 1983. Google Scholar
  26. J.R. Norris. Markov Chains. Cambridge, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact