Document Open Access Logo

Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking

Authors Jakob Piribauer , Christel Baier , Nathalie Bertrand , Ocan Sankur

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.7.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Author Details

Jakob Piribauer
  • Technische Universität Dresden, Germany
Christel Baier
  • Technische Universität Dresden, Germany
Nathalie Bertrand
  • Université Rennes, Inria, CNRS, IRISA, France
Ocan Sankur
  • Université Rennes, Inria, CNRS, IRISA, France

Funding

This work was funded by DFG grant 389792660 as part of TRR 248 – CPEC (see https://perspicuous- computing.science), the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), DFG-projects BA-1679/11-1 and BA- 1679/12-1, and the Research Training Group QuantLA (GRK 1763).

Cite AsGet BibTex

Jakob Piribauer, Christel Baier, Nathalie Bertrand, and Ocan Sankur. Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.7

Abstract

Quantified linear temporal logic (QLTL) is an ω-regular extension of LTL allowing quantification over propositional variables. We study the model checking problem of QLTL-formulas over Markov chains and Markov decision processes (MDPs) with respect to the number of quantifier alternations of formulas in prenex normal form. For formulas with k{-}1 quantifier alternations, we prove that all qualitative and quantitative model checking problems are k-EXPSPACE-complete over Markov chains and k{+}1-EXPTIME-complete over MDPs. As an application of these results, we generalize vacuity checking for LTL specifications from the non-probabilistic to the probabilistic setting. We show how to check whether an LTL-formula is affected by a subformula, and also study inherent vacuity for probabilistic systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Quantified linear temporal logic
  • Markov chain
  • Markov decision process
  • vacuity

Metrics

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

Related Versions

References

  1. Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, and Moshe Y. Vardi. Enhanced vacuity detection in linear temporal logic. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), volume 2725 of Lecture Notes in Computer Science, pages 368-380. Springer, 2003. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  3. Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh. Efficient detection of vacuity in temporal model checking. Formal Methods in System Design, 18(2):141-163, 2001. Google Scholar
  4. Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, and Moshe Y. Vardi. Regular vacuity. In Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'05), volume 3725 of Lecture Notes in Computer Science, pages 191-206. Springer, 2005. Google Scholar
  5. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  6. Edmund Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 2000. Google Scholar
  7. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857-907, 1995. Google Scholar
  8. Bernd Finkbeiner and Leander Tentrup. Detecting unrealizability of distributed fault-tolerant systems. Logical Methods in Computer Science, 11(3):1-31, 2015. URL: https://doi.org/10.2168/LMCS-11(3:12)2015.
  9. Dana Fisman, Orna Kupferman, Sarai Sheinvald-Faragy, and Moshe Y. Vardi. A framework for inherent vacuity. In Proceedings of the 4th International Haifa Verification Conference (HVC'08), volume 5394 of Lecture Notes in Computer Science, pages 7-22. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-01702-5_7.
  10. Dov Gabbay. The declarative past and imperative future. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, pages 409-448, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. Google Scholar
  11. Arie Gurfinkel and Marsha Chechik. Extending extended vacuity. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 306-321. Springer, 2004. Google Scholar
  12. Arie Gurfinkel and Marsha Chechik. How vacuous is vacuous? In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), pages 451-466, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  13. Walter Hussak. Serializable histories in quantified propositional temporal logic. International Journal of Computer Mathematics, 81(10):1203-1211, 2004. URL: https://doi.org/10.1080/00207160412331284051.
  14. Yonit Kesten and Amir Pnueli. Complete proof system for QPTL. Journal of Logic and Computation, 12(5):701-745, 2002. Google Scholar
  15. Orna Kupferman. Sanity checks in formal verification. In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR'06), volume 4137 of Lecture Notes in Computer Science, pages 37-51. Springer, 2006. Google Scholar
  16. Orna Kupferman and Moshe Y. Vardi. Vacuity detection in temporal model checking. International Journal on Software Tools for Technology Transfer, 4(2):224-233, 2003. Google Scholar
  17. François Laroussinie and Nicolas Markey. Quantified CTL: Expressiveness and Complexity. Logical Methods in Computer Science, 10(4):1-45, 2014. URL: https://doi.org/10.2168/LMCS-10(4:17)2014.
  18. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  19. Jakob Piribauer, Christel Baier, Nathalie Bertrand, and Ocan Sankur. Quantified linear temporal logic over probabilistic systems with an application to vacuity checking (extended version). Technical report, TU Dresden, Dresden, Germany, 2021. See URL: https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/CONCUR21/.
  20. Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York, NY, 1994. Google Scholar
  21. A. Prasad Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Carnegie-Mellon University, 1983. Google Scholar
  22. A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49(2-3):217-237, 1987. Google Scholar
  23. Aravinda P. Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  24. Peter van Emde Boas. The convenience of tilings. Lecture Notes in Pure and Applied Mathematics, pages 331-363, 1997. Google Scholar
  25. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the 1st Symposium on Logic in Computer Science (LICS'86), pages 332-344. IEEE Computer Society Press, 1986. Google Scholar
  26. Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
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