Document Open Access Logo

A Decidable Non-Regular Modal Fixpoint Logic

Authors Florian Bruse, Martin Lange

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.23.pdf
  • Filesize: 0.7 MB
  • 18 pages

Document Identifiers

Author Details

Florian Bruse
  • School of Electrical Engineering and Computer Science, Universität Kassel, Germany
Martin Lange
  • School of Electrical Engineering and Computer Science, Universität Kassel, Germany

Cite AsGet BibTex

Florian Bruse and Martin Lange. A Decidable Non-Regular Modal Fixpoint Logic. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.23

Abstract

Fixpoint Logic with Chop (FLC) extends the modal μ-calculus with an operator for sequential composition between predicate transformers. This makes it an expressive modal fixpoint logic which is capable of formalising many non-regular program properties. Its satisfiability problem is highly undecidable. Here we define Visibly Pushdown Fixpoint Logic with Chop, a fragment in which fixpoint formulas are required to be of a certain form resembling visibly pushdown grammars. We give a sound and complete game-theoretic characterisation of FLC’s satisfiability problem and show that the games corresponding to formulas from this fragment are stair-parity games and therefore effectively solvable, resulting in 2EXPTIME-completeness of this fragment. The lower bound is inherited from PDL over Recursive Programs, which is structurally similar but considerably weaker in expressive power.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Program specifications
Keywords
  • formal specification
  • temporal logic
  • expressive power

Metrics

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

References

  1. E. Alsmann, F. Bruse, and M. Lange. Separating the expressive power of propositional dynamic and modal fixpoint logics, 2021. Submitted. Google Scholar
  2. R. Alur and P. Madhusudan. Visibly pushdown languages. In Proc. 36th Annual ACM Symp. on Theory of Computing, STOC'04, pages 202-211. ACM, 2004. URL: https://doi.org/10.1145/1007352.1007390.
  3. J. Baran and H. Barringer. A grammatical representation of visibly pushdown languages. In Proc. 14th Int. Workshop on Logic, Language, Information and Computation, WoLLIC'07, volume 4576 of LNCS, pages 1-11. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73445-1_1.
  4. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In Proc. 49th Annual ACM SIGACT Symp. on Theory of Computing, STOC'17, pages 252-263. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055409.
  5. E. A. Emerson and C. S. Jutla. Tree automata, μ-calculus and determinacy. In Proc. 32nd Symp. on Foundations of Computer Science, pages 368-377, San Juan, Puerto Rico, 1991. IEEE. URL: https://doi.org/10.1109/sfcs.1991.185392.
  6. E. A. Emerson and C. S. Jutla. The complexity of tree automata and logics of programs. SIAM Journal on Computing, 29(1):132-158, 2000. URL: https://doi.org/10.1137/s0097539793304741.
  7. M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  8. O. Friedmann, F. Klaedtke, and M. Lange. Ramsey-based inclusion checking for visibly pushdown automata. ACM Trans. Comput. Log., 16(4):34, 2015. URL: https://doi.org/10.1145/2774221.
  9. O. Friedmann and M. Lange. The modal μ-calculus caught off guard. In 20th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'11, volume 6793 of LNCS, pages 149-163. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22119-4_13.
  10. D. Harel, A. Pnueli, and J. Stavi. Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences, 26(2):222-243, 1983. URL: https://doi.org/10.1016/0022-0000(83)90014-4.
  11. D. Harel and D. Raz. Deciding properties of nonregular programs (preliminary version). In Proc. 31st Annual Symp. on Foundations of Computer Science, FOCS'90, volume II, pages 652-661, St. Louis, Missouri, 1990. IEEE. URL: https://doi.org/10.1109/fscs.1990.89587.
  12. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic. In CONCUR, pages 263-277, 1996. URL: https://doi.org/10.1007/3-540-61604-7_60.
  13. M. Jurdziński. Small progress measures for solving parity games. In H. Reichel and S. Tison, editors, Proc. 17th Ann. Symp. on Theoretical Aspects of Computer Science, STACS'00, volume 1770 of LNCS, pages 290-301. Springer, 2000. URL: https://doi.org/10.1007/3-540-46541-3_24.
  14. T. Koren and A. Pnueli. There exist decidable context free propositional dynamic logics. In E. Clarke and D. Kozen, editors, Proc. of the Workshop on Logics of Programs, volume 164 of LNCS, pages 290-312. Springer, 1983. URL: https://doi.org/10.1007/3-540-12896-4_369.
  15. D. Kozen. Results on the propositional μ-calculus. TCS, 27:333-354, 1983. URL: https://doi.org/10.1007/BFb0012782.
  16. D. Kozen and R. Parikh. A decision procedure for the propositional μ-calculus. In Proc. Workshop on Logics of Programs, volume 164 of LNCS, pages 313-325. Springer, 1983. URL: https://doi.org/10.1007/3-540-12896-4_370.
  17. M. Lange. Local model checking games for fixed point logic with chop. In Proc. 13th Conf. on Concurrency Theory, CONCUR'02, volume 2421 of LNCS, pages 240-254. Springer, 2002. URL: https://doi.org/10.1007/3-540-45694-5_17.
  18. M. Lange. Temporal logics beyond regularity, 2007. Habilitation thesis, University of Munich, BRICS research report RS-07-13. URL: https://doi.org/10.7146/brics.v14i13.22178.
  19. M. Lange and R. Somla. Propositional dynamic logic of context-free programs and fixpoint logic with chop. Information Processing Letters, 100(2):72-75, 2006. URL: https://doi.org/10.1016/j.ipl.2006.04.019.
  20. C. Löding, C. Lutz, and O. Serre. Propositional dynamic logic with recursive programs. J. Log. Algebr. Program, 73(1-2):51-69, 2007. URL: https://doi.org/10.1016/j.jlap.2006.11.003.
  21. C. Löding, P. Madhusudan, and O. Serre. Visibly pushdown games. In Proc. 24th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'04, volume 3328 of LNCS, pages 408-420. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_34.
  22. A.W. Mostowski. Games with forbidden positions. Technical Report 78, Uniwersytet Gdański. Instytut Matematyki, 1991. Google Scholar
  23. M. Müller-Olm. A modal fixpoint logic with chop. In Proc. 16th Symp. on Theoretical Aspects of Computer Science, STACS'99, volume 1563 of LNCS, pages 510-520. Springer, 1999. URL: https://doi.org/10.1007/3-540-49116-3_48.
  24. D. Niwiński and I. Walukiewicz. Games for the μ-calulus. TCS, 163:99-116, 1997. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  25. R. S. Streett. Propositional dynamic logic of looping and converse. In Proc. 13th Symp. on Theory of Computation, STOC'81, pages 375-383. ACM, 1981. URL: https://doi.org/10.1145/800076.802492.
  26. R. S. Streett and E. A. Emerson. An automata theoretic decision procedure for the propositional μ-calculus. Information and Computation, 81(3):249-264, 1989. URL: https://doi.org/10.1016/0890-5401(89)90031-x.
  27. A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 5:285-309, 1955. URL: https://doi.org/10.2140/pjm.1955.5.285.
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