Document Open Access Logo

Global Caching for the Alternation-free µ-Calculus

Authors Daniel Hausmann, Lutz Schröder, Christoph Egger

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.34.pdf
  • Filesize: 0.56 MB
  • 15 pages

Document Identifiers

Author Details

Daniel Hausmann
Lutz Schröder
Christoph Egger

Cite AsGet BibTex

Daniel Hausmann, Lutz Schröder, and Christoph Egger. Global Caching for the Alternation-free µ-Calculus. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 34:1-34:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.34

Abstract

We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free mu-calculus. The algorithm supports global caching with intermediate propagation and runs in time 2^O(n). In game-theoretic terms, our algorithm integrates the steps for constructing and solving the Büchi game arising from the input tableau into a single procedure; this is done on-the-fly, i.e. may terminate before the game has been fully constructed. This suggests a slogan to the effect that global caching = game solving on-the-fly. A prototypical implementation shows promising initial results.
Keywords
  • modal logic
  • fixpoint logic
  • satisfiability
  • global caching
  • coalgebraic logic

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. Dietmar Berwanger, Erich Grädel, and Giacomo Lenzi. The variable hierarchy of the μ-calculus is strict. Theory Comput. Sys., 40:437-466, 2007. Google Scholar
  3. Julian Bradfield and Colin Stirling. Modal μ-calculi. In Handbook of Modal Logic, pages 721-756. Elsevier, 2006. Google Scholar
  4. Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. J. Log. Algebr. Prog., 76:216-225, 2008. Google Scholar
  5. Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus. Log. Meth. Comput. Sci., 7, 2011. Google Scholar
  6. 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
  7. Edmund Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logics of Programs, volume 131 of LNCS, pages 52-71. Springer, 1982. Google Scholar
  8. Amélie David. TATL: Implementation of ATL tableau-based decision procedure. In Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013, volume 8123 of LNCS, pages 97-103. Springer, 2013. Google Scholar
  9. E. Allen Emerson and Joseph Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Sys. Sci., 30:1-24, 1985. Google Scholar
  10. E. Allen Emerson and Charanjit Jutla. The complexity of tree automata and logics of programs. SIAM J. Comput., 29(1):132-158, September 1999. Google Scholar
  11. Oliver Friedmann and Martin Lange. Local strategy improvement for parity game solving. In Games, Automata, Logic, and Formal Verification, GANDALF 2010, volume 25 of EPTCS, pages 118-131. Open Publishing Association, 2010. Google Scholar
  12. Oliver Friedmann and Martin Lange. A solver for modal fixpoint logics. In Methods for Modalities, M4M-6 2009, volume 262 of ENTCS, pages 99-111, 2010. Google Scholar
  13. Oliver Friedmann and Martin Lange. Deciding the unguarded modal μ-calculus. J. Appl. Non-Classical Log., 23:353-371, 2013. Google Scholar
  14. Oliver Friedmann, Markus Latte, and Martin Lange. Satisfiability games for branching-time logics. Log. Methods Comput. Sci., 9, 2013. Google Scholar
  15. Rajeev Goré. And-Or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In Automated Reasoning, IJCAR 2014, volume 8562 of LNCS, pages 26-45. Springer, 2014. Google Scholar
  16. Rajeev Goré, Clemens Kupke, and Dirk Pattinson. Optimal tableau algorithms for coalgebraic logics. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, volume 6015 of LNCS, pages 114-128. Springer, 2010. Google Scholar
  17. Rajeev Goré, Clemens Kupke, Dirk Pattinson, and Lutz Schröder. Global caching for coalgebraic description logics. In Automated Reasoning, IJCAR 2010, volume 6173 of LNCS, pages 46-60. Springer, 2010. Google Scholar
  18. Rajeev Goré and Linh Anh Nguyen. Exptime tableaux for ALC using sound global caching. J. Autom. Reasoning, 50:355-381, 2013. Google Scholar
  19. Rajeev Goré, Jimmy Thomson, and Florian Widmann. An experimental comparison of theorem provers for CTL. In Temporal Representation and Reasoning, TIME 2011, pages 49-56. IEEE, 2011. Google Scholar
  20. Rajeev Goré and Florian Widmann. An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In Automated Deduction, CADE 2009, volume 5663 of LNCS, pages 437-452. Springer, 2009. Google Scholar
  21. Rajeev Goré and Florian Widmann. Sound global state caching for ALC with inverse roles. In Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, volume 5607 of LNCS, pages 205-219. Springer, 2009. Google Scholar
  22. Daniel Gorín, Dirk Pattinson, Lutz Schröder, Florian Widmann, and Thorsten Wißmann. COOL - a generic reasoner for coalgebraic hybrid logics (system description). In Automated Reasoning, IJCAR 2014, volume 8562 of LNCS, pages 396-402. Springer, 2014. Google Scholar
  23. Daniel Hausmann and Lutz Schröder. Global caching for the flat coalgebraic μ-calculus. In Temporal Representation and Reasoning, TIME 2015, pages 121-143. IEEE, 2015. Google Scholar
  24. Natthapong Jungteerapanich. A tableau system for the modal μ-calculus. In Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, volume 5607 of LNCS, pages 220-234. Springer, 2009. Google Scholar
  25. Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983. Google Scholar
  26. Dexter Kozen. A finite model theorem for the propositional μ-calculus. Stud. Log., 47:233-241, 1988. Google Scholar
  27. Martin Lange and Colin Stirling. Focus games for satisfiability and completeness of temporal logic. In Logic in Computer Science, LICS 2001, pages 357-365. IEEE Computer Society, 2001. Google Scholar
  28. Zohar Manna and Amir Pnueli. The modal logic of programs. In Automata, Languages and Programming, ICALP 1979, volume 71 of LNCS, pages 385-409. Springer, 1979. Google Scholar
  29. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theoret. Comput. Sci., 32:321-330, 1984. Google Scholar
  30. Marco Montali, Paolo Torroni, Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, and Paola Mello. Verification from declarative specifications using logic programming. In Logic Programming, ICLP 2008, volume 5366 of LNCS, pages 440-454. Springer, 2008. Google Scholar
  31. Damian Niwinski and Igor Walukiewicz. Games for the μ-calculus. Theor. Comput. Sci., 163:99-116, 1996. Google Scholar
  32. Rohit Parikh. The logic of games and its applications. Ann. Discr. Math., 24:111-140, 1985. Google Scholar
  33. Amir Pnueli. The temporal logic of programs. In Foundations of Computer Science, FOCS 1977, pages 46-57. IEEE Computer Society, 1977. Google Scholar
  34. Vaughan Pratt. Semantical considerations on Floyd-Hoare logic. In Foundations of Computer Science, FOCS 1976, pages 109-121. IEEE Computer Society, 1976. Google Scholar
  35. Shmuel Safra. On the complexity of omega-automata. In Foundations of Computer Science, FOCS 1988, pages 319-327. IEEE Computer Society, 1988. Google Scholar
  36. Sven Schewe. Synthesis of distributed systems. PhD thesis, Universität des Saarlands, 2008. Google Scholar
  37. Lan Zhang, Ullrich Hustadt, and Clare Dixon. A resolution calculus for the branching-time temporal logic CTL. ACM Trans. Comput. Log., 15, 2014. 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact