Document Open Access Logo

Temporal Logic with Recursion

Authors Florian Bruse, Martin Lange

PDF
Thumbnail PDF

File

LIPIcs.TIME.2020.6.pdf
  • Filesize: 467 kB
  • 14 pages

Document Identifiers

Author Details

Florian Bruse
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany
Martin Lange
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany

Cite AsGet BibTex

Florian Bruse and Martin Lange. Temporal Logic with Recursion. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TIME.2020.6

Abstract

We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments. Unlike other proposals for modal fixpoint logics of high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet have expressive power beyond that of the modal μ-calculus or MSO. We advocate these logics by showing how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues of the standard decision problems.

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. R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181-204, 1994. 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. A. Arnold and D. Niwiński. Rudiments of μ-calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2001. Google Scholar
  4. R. Axelsson, M. Lange, and R. Somla. The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science, 3:1-33, 2007. Google Scholar
  5. H. Bekić. Programming Languages and Their Definition, Selected Papers, volume 177 of LNCS. Springer, 1984. Google Scholar
  6. J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60(1-3):109-137, 1984. Google Scholar
  7. E. A. Emerson. Uniform inevitability is tree automaton ineffable. Information Processing Letters, 24(2):77-79, 1987. Google Scholar
  8. E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982. Google Scholar
  9. E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30:1-24, 1985. Google Scholar
  10. E. A. Emerson and J. Y. Halpern. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  11. 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. Google Scholar
  12. M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. Google Scholar
  13. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512-535, 1994. Google Scholar
  14. D. Harel. Recurring dominoes: Making the highly undecidable highly understandable. Annals of Discrete Mathematics, 24:51-72, 1985. Google Scholar
  15. D. Harel, A. Pnueli, and J. Stavi. Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences, 26(2):222-243, 1983. Google Scholar
  16. 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.
  17. B. Knaster. Un théorème sur les fonctions d'ensembles. Annals Soc. Pol. Math, 6:133-134, 1928. Google Scholar
  18. R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, November 1990. Google Scholar
  19. D. Kozen. Results on the propositional μ-calculus. TCS, 27:333-354, December 1983. URL: https://doi.org/10.1007/BFb0012782.
  20. D. Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, 1988. Google Scholar
  21. L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, 1994. Google Scholar
  22. 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. Google Scholar
  23. M. Lange. Temporal logics beyond regularity, 2007. Habilitation thesis, University of Munich, BRICS research report RS-07-13. Google Scholar
  24. M. Lange. Three notes on the complexity of model checking fixpoint logic with chop. R.A.I.R.O. - Theoretical Informatics and Applications, 41:177-190, 2007. Google Scholar
  25. 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. Google Scholar
  26. C. Löding, C. Lutz, and O. Serre. Propositional dynamic logic with recursive programs. J. Log. Algebr. Program, 73(1-2):51-69, 2007. Google Scholar
  27. 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. Google Scholar
  28. M. Müller-Olm. A modal fixpoint logic with chop. In STACS'99, volume 1563 of LNCS, pages 510-520. Springer, 1999. Google Scholar
  29. A. Pnueli. The temporal logic of programs. In Proc. 18th Symp. on Foundations of Computer Science, FOCS'77, pages 46-57, Providence, RI, USA, 1977. IEEE. Google Scholar
  30. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. Google Scholar
  31. C. Stirling. Comparing linear and branching time temporal logics. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Conf. on Temporal Logic in Specification, volume 398 of LNCS, pages 1-20, Berlin, 1989. Springer. Google Scholar
  32. A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  33. M. Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc. 17th Symp. on Theory of Computing, STOC'85, pages 240-251, Baltimore, USA, 1985. ACM. Google Scholar
  34. M. Viswanathan and R. Viswanathan. A higher order modal fixed point logic. In CONCUR'04, volume 3170 of LNCS, pages 512-528. Springer, 2004. 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