Separable GPL: Decidable Model Checking with More Non-Determinism

Authors Andrey Gorlin, C. R. Ramakrishnan



PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Andrey Gorlin
  • Stony Brook University, Department of Computer Science, Stony Brook, N.Y. 11794, USA
C. R. Ramakrishnan
  • Stony Brook University, Department of Computer Science, Stony Brook, N.Y. 11794, USA

Cite As Get BibTex

Andrey Gorlin and C. R. Ramakrishnan. Separable GPL: Decidable Model Checking with More Non-Determinism. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.36

Abstract

Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of branching probabilistic systems. We consider GPL over branching systems that also exhibit internal non-determinism under linear-time semantics (which is resolved by schedulers), and focus on the problem of finding the capacity (supremum probability over all schedulers) of a fuzzy formula. Model checking GPL is undecidable, in general, over such systems, and existing GPL model checking algorithms are limited to systems without internal non-determinism, or to checking non-recursive formulae. We define a subclass, called separable GPL, which includes recursive formulae and for which model checking is decidable. A large class of interesting and decidable problems, such as termination of 1-exit Recursive MDPs, reachability of Branching MDPs, and LTL model checking of MDPs, whose decidability has been studied independently, can be reduced to model checking separable GPL. Thus, GPL is widely applicable and, with a suitable extension of its semantics, yields a uniform framework for studying problems involving systems with non-deterministic and probabilistic behaviors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Modal mu-calculus
  • probabilistic logics
  • probabilistic systems
  • branching systems
  • model checking

Metrics

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

References

  1. Rajeev Alur, Swarat Chaudhuri, and P. Madhusudan. Software model checking using languages of nested trees. ACM Trans. Program. Lang. Syst., 33(5):15:1-15:45, November 2011. Google Scholar
  2. Christel Baier. On algorithmic verification methods for probabilistic systems. Habilitation thesis, Fakultät für Mathematik &Informatik, Universität Mannheim, 1998. Google Scholar
  3. Pablo Castro, Cecilia Kilmurray, and Nir Piterman. Tractable probabilistic mu-calculus that expresses probabilistic temporal logics. In STACS, volume 30 of LIPIcs, pages 211-223. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  4. Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. In MFCS, pages 271-282, Berlin, Heidelberg, 2012. Springer. Google Scholar
  5. Rance Cleaveland, S. Purushothaman Iyer, and Murali Narasimha. Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science, 342(2-3):316-350, 2005. Google Scholar
  6. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Weak bisimulation is sound and complete for PCTL*. In CONCUR, volume 2421 of LNCS, pages 355-370. Springer Berlin Heidelberg, 2002. Google Scholar
  7. Javier Esparza, Antonín Kucera, and Richard Mayr. Model checking probabilistic pushdown automata. In LICS, pages 12-21, 2004. Google Scholar
  8. Kousha Etessami, Alistair Stewart, and Mihalis Yannakakis. Polynomial time algorithms for branching Markov decision processes and probabilistic min(max) polynomial Bellman equations. In ICALP, Part I, pages 314-326, Berlin, Heidelberg, 2012. Springer. Google Scholar
  9. Kousha Etessami, Alistair Stewart, and Mihalis Yannakakis. Polynomial time algorithms for multi-type branching processes and stochastic context-free grammars. In STOC, pages 579-588. ACM, 2012. Google Scholar
  10. Kousha Etessami, Alistair Stewart, and Mihalis Yannakakis. Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes. In ICALP, Part II, pages 184-196, Berlin, Heidelberg, 2015. Springer. Google Scholar
  11. Kousha Etessami and Mihalis Yannakakis. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM, 56(1):1:1-1:66, February 2009. Google Scholar
  12. Kousha Etessami and Mihalis Yannakakis. Recursive Markov decision processes and recursive stochastic games. J. ACM, 62(2):11:1-11:69, May 2015. Google Scholar
  13. Diana Fischer, Erich Grädel, and Łukasz Kaiser. Model checking games for the quantitative μ-calculus. Theory of Computing Systems, 47(3):696-719, 2010. Google Scholar
  14. Tomasz Gogacz, Henryk Michalewski, Matteo Mio, and Michał Skrzypczak. Measure properties of regular sets of trees. Information and Computation, 256:108 - 130, 2017. URL: http://www.sciencedirect.com/science/article/pii/S0890540117300627, URL: http://dx.doi.org/https://doi.org/10.1016/j.ic.2017.04.012.
  15. Andrey Gorlin and C. R. Ramakrishnan. XPL: an extended probabilistic logic for probabilistic transition systems. CoRR, abs/1604.06118, 2016. Google Scholar
  16. Andrey Gorlin, C. R. Ramakrishnan, and Scott A. Smolka. Model checking with probabilistic tabled logic programming. TPLP, 12(4-5):681-700, 2012. Google Scholar
  17. Wanwei Liu, Lei Song, Ji Wang, and Lijun Zhang. A simple probabilistic extension of modal mu-calculus. In IJCAI, 2015. Google Scholar
  18. Annabelle McIver and Carroll Morgan. Results on the quantitative μ-calculus qMμ. ACM Trans. Comput. Logic, 8(1), January 2007. Google Scholar
  19. Henryk Michalewski and Matteo Mio. On the problem of computing the probability of regular sets of trees. In FSTTCS, volume 45 of LIPIcs, pages 489-502. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  20. Matteo Mio. Game semantics for probabilistic modal mu-calculi. PhD thesis, The University of Edinburgh, 2012. Google Scholar
  21. Matteo Mio. Probabilistic modal μ-calculus with independent product. Logical Methods in Computer Science, Volume 8, Issue 4, November 2012. URL: https://lmcs.episciences.org/789, URL: http://dx.doi.org/10.2168/LMCS-8(4:18)2012.
  22. Matteo Mio and Alex Simpson. Łukasiewicz mu-calculus. In FICS, volume 126 of EPTCS, pages 87-104, 2013. Google Scholar
  23. Marcin Przybylko and Michal Skrzypczak. On the complexity of branching games with regular conditions. In LIPIcs, volume 58. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  24. Roberto Segala. A compositional trace-based semantics for probabilistic automata. In CONCUR, pages 234-248, 1995. Google Scholar
  25. Roberto Segala and Andrea Turrini. Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In QEST, pages 44-53. IEEE Computer Society, 2005. Google Scholar
  26. Arvind Soni. Probabilistic and nondeterministic systems. Masters thesis, North Carolina State University, 2004. Google Scholar
  27. Alfred Tarski. A decision method for elementary algebra and geometry. Bulletin of the American Mathematical Society, 59, 1951. 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