Document Open Access Logo

Complexity of Model Checking MDPs against LTL Specifications

Authors Dileep Kini, Mahesh Viswanathan

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.35.pdf
  • Filesize: 0.52 MB
  • 13 pages

Document Identifiers

Author Details

Dileep Kini
Mahesh Viswanathan

Cite As Get BibTex

Dileep Kini and Mahesh Viswanathan. Complexity of Model Checking MDPs against LTL Specifications. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 35:1-35:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.35

Abstract

Given a Markov Decision Process (MDP) M, an LTL formula \varphi, and a threshold \theta \in [0,1], the verification question is to determine if there is a scheduler with respect to which the executions of M satisfying \varphi have probability greater than (or greater than or equal to) \theta. When \theta = 0, we call it the qualitative verification problem, and when \theta \in (0,1], we call it the quantitative verification problem. In this paper we study the precise complexity of these problems when the specification is constrained to be in different fragments of LTL.

Subject Classification

Keywords
  • Markov Decision Processes
  • Linear Temporal Logic
  • model checking
  • complexity

Metrics

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

References

  1. R. Alur and S. La Torre. Deterministic generators and games for LTL fragments. ACM Trans. Comput. Logic, 5(1):1-25, 2004. Google Scholar
  2. R. Alur, S. La Torre, and P. Madhusudan. Playing games with boxes and diamonds. In Proceedings of the International Conference on Concurrency Theory, pages 128-143, 2003. Google Scholar
  3. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  4. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. Journal of the ACM (JACM), 42(4):857-907, 1995. Google Scholar
  5. Dileep Kini and Mahesh Viswanathan. Limit deterministic and probabilistic automata for LTL backslash GU. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 628-642, 2015. Google Scholar
  6. Dileep Kini and Mahesh Viswanathan. Optimal translation of LTL to limit deterministic automata. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 113-129, 2017. Google Scholar
  7. J. Marcinkowski and T. Truderung. Optimal complexity bounds for positive LTL games. In Proceedings of the International Conference on Computer Science Logic, pages 262-275, 2002. Google Scholar
  8. A. Pnueli. The temporal logic of programs. In Proceedings of the Annual Symposium on Foundations of Computer Science, pages 46-57, 1977. Google Scholar
  9. M.L. Puterman. Markov Decision Processes. Wiley, 1994. Google Scholar
  10. Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínskỳ. Limit-deterministic Büchi automata for linear temporal logic. In Proceedings of the International Conference on Computer-Aided Verification, pages 312-332, 2016. Google Scholar
  11. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Proceedings of the 26th Annual Symposium on Foundations of Computer Science, pages 327-338. IEEE Computer Society, 1985. 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 About DROPS Imprint Privacy Contact