Document Open Access Logo

Game-Based Local Model Checking for the Coalgebraic mu-Calculus

Authors Daniel Hausmann, Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.35.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Daniel Hausmann
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

Work forms part of the DFG project Generic Algorithmic Methods for Modal and Hybrid Logics (SCHR 1118/5-3).

Cite AsGet BibTex

Daniel Hausmann and Lutz Schröder. Game-Based Local Model Checking for the Coalgebraic mu-Calculus. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.35

Abstract

The coalgebraic mu-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational mu-calculus, such diverse logics as the graded mu-calculus, the monotone mu-calculus, the probabilistic mu-calculus, and the alternating-time mu-calculus. In the present work, we give a local model checking algorithm for the coalgebraic mu-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in time p^k where p is a polynomial in the formula and model size and where k is the alternation depth of the formula. We show moreover that under the same assumptions, the model checking problem is in both NP and coNP, improving the complexity in all mentioned non-relational cases. If one-step satisfaction can be solved by means of small finite games, we moreover obtain standard parity games, ensuring quasi-polynomial run time. This applies in particular to the monotone mu-calculus, the alternating-time mu-calculus, and the graded mu-calculus with grades coded in unary.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • Model checking
  • mu-calculus
  • coalgebraic logic
  • graded mu-calculus
  • probabilistic mu-calculus
  • parity games

Metrics

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

References

  1. Rajeev Alur, Thomas Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49:672-713, 2002. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Florian Bruse, Michael Falk, and Martin Lange. The Fixpoint-Iteration Algorithm for Parity Games. In Games, Automata, Logics and Formal Verification, GandALF 2014, volume 161 of EPTCS, pages 116-130, 2014. Google Scholar
  4. Cristian Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Theory of Computing, STOC 2017, pages 252-263. ACM, 2017. Google Scholar
  5. Brian F. Chellas. Modal Logic. Cambridge University Press, 1980. Google Scholar
  6. Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus. In Computer Science Logic, CSL 2009, volume 5771 of LNCS, pages 179-193. Springer, 2009. Google Scholar
  7. Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus. Log. Meth. Comput. Sci., 7, 2011. Google Scholar
  8. Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. Comput. J., 54:31-41, 2011. Google Scholar
  9. Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo. Parity Automata for Quantitative Linear Time Logics. In Algebra and Coalgebra in Computer Science, CALCO 2017, volume 72 of LIPIcs, pages 7:1-7:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: http://www.dagstuhl.de/dagpub/978-3-95977-033-0.
  10. Giovanna D'Agostino and Albert Visser. Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Logic, 41:267-298, 2002. Google Scholar
  11. E. Allen Emerson, Charanjit Jutla, and A. Prasad Sistla. On model checking for the μ-calculus and its fragments. Theor. Comput. Sci., 258:491-522, 2001. URL: http://dx.nodoi.org/10.1016/S0304-3975(00)00034-7.
  12. Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. Monadic Second-Order Logic and Bisimulation Invariance for Coalgebras. In Logic in Computer Science, LICS 2015. IEEE, 2015. Google Scholar
  13. Alessandro Ferrante, Aniello Murano, and Mimmo Parente. Enriched μ-Calculi Module Checking. Log. Methods Comput. Sci., 4(3), 2008. Google Scholar
  14. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36387-4.
  15. Helle Hvid Hansen, Clemens Kupke, Johannes Marti, and Yde Venema. Parity Games and Automata for Game Logic. In Dynamic Logic. New Trends and Applications, DALI 2017, volume 10669 of LNCS, pages 115-132. Springer, 2018. Google Scholar
  16. Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic Progress Measures and Coalgebraic Model Checking. In Principles of Programming Languages, POPL 2016, pages 718-732. ACM, 2016. Google Scholar
  17. Daniel Hausmann and Lutz Schröder. Optimal Satisfiability Checking for Arithmetic μ-Calculi. In Foundations of Software Science and Computation Structures, FOSSACS 2019, volume 11425 of LNCS, pages 277-294. Springer, 2019. Google Scholar
  18. Marcin Jurdziński. Small Progress Measures for Solving Parity Games. In Horst Reichel and Sophie Tison, editors, Symposium on Theoretical Aspects of Computer Science, STACS 2000, pages 290-301, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  19. Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983. Google Scholar
  20. Orna Kupferman, Ulrike Sattler, and Moshe Vardi. The Complexity of the Graded μ-Calculus. In Automated Deduction, CADE 02, volume 2392 of LNCS, pages 423-437. Springer, 2002. Google Scholar
  21. Wanwei Liu, Lei Song, Ji Wang, and Lijun Zhang. A Simple Probabilistic Extension of Modal Mu-calculus. In International Joint Conference on Artificial Intelligence, IJCAI 2015, pages 882-888. AAAI Press, 2015. Google Scholar
  22. Damian Niwinski. On Fixed-Point Clones (Extended Abstract). In Automata, Languages and Programming, ICALP 1986, volume 226 of LNCS, pages 464-473. Springer, 1986. Google Scholar
  23. Rohit Parikh. The logic of games and its applications. Ann. Discr. Math., 24:111-140, 1985. Google Scholar
  24. Marc Pauly. A Modal Logic for Coalitional Power in Games. J. Logic Comput., 12:149-166, 2002. Google Scholar
  25. David Peleg. Concurrent dynamic logic. J. ACM, 34:450-479, 1987. URL: http://nodoi.acm.org/10.1145/23005.23008.
  26. Jan Rutten. Universal Coalgebra: A Theory of Systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  27. Philippe Schnoebelen. The Complexity of Temporal Logic Model Checking. In Advances in Modal Logic, AiML 2002, pages 393-436. College Publications, 2003. Google Scholar
  28. Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In Theoretical Aspects of Computer Science, STACS 09, pages 673-684. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; Dagstuhl, Germany, 2009. Google Scholar
  29. Lutz Schröder and Yde Venema. Completeness of Flat Coalgebraic Fixpoint Logics. ACM Trans. Comput. Log., 19(1):4:1-4:34, 2018. Google Scholar
  30. Colin Stirling and David Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161-177, 1991. 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