Abstract
The linear time μ-calculus extends LTL with arbitrary least and greatest fixpoint operators. This gives it the power to express all ω-regular languages, i.e. strictly more than LTL. The validity problem is PSPACE-complete for both LTL and the linear time μ-calculus. In practice it is more difficult for the latter because of nestings of fixpoint operators and variables with several occurrences.
We present a simple sound and complete infinitary proof system for the linear time μ-calculus and then present two decision procedures for provability in the system, hence validity of formulas. One uses nondeterministic Büchi automata, the other one a generalisation of size-change termination analysis (SCT) known from functional programming.
The main novelties of this paper are the connection with SCT and the fact that both decision procedures have a better asymptotic complexity than earlier ones and have been implemented.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Conf. Record of the 13th Annual ACM Symp. on Principles of Programming Languages, POPL 1986, pp. 173–183. ACM, New York (1986)
Bradfield, J.C., Esparza, J., Mader, A.: An effective tableau system for the linear time μ-calculus. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 98–109. Springer, Heidelberg (1996)
Dax, C.: Games for the linear time μ-calculus. Master’s thesis, Dep. of Computer Science, University of Munich (2006), Available from: http://www.tcs.ifi.lmu.de/lehre/da_fopra/Christian_Dax.pdf
Kaivola, R.: A simple decision method for the linear time μ-calculus. In: Proc. Int. Workshop on Structures in Conc. Theory, STRICT 1995, pp. 190–204 (1995)
Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: Proc. 32nd Annual Symp. on Foundations of Computer Science, FOCS 1991, pp. 358–367. IEEE, Los Alamitos (1991)
Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Proc. 30th Annual ACM Symp. on Theory of Computing, STOC 1998, pp. 224–233. ACM Press, New York (1998)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. J-SIGPLAN 36(3), 81–92 (2001)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Proc. 21st Ann. IEEE Symp. on Logic in Computer Science, LICS 2006. IEEE Computer Society Press, Los Alamitos (to appear, 2006)
Safra, S.: On the complexity of ω-automata. In: Proc. 29th Symp. on Foundations of Computer Science, FOCS 1988, pp. 319–327. IEEE, Los Alamitos (1988)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery 32(3), 733–749 (1985)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. TCS 49(2-3), 217–237 (1987)
Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional μ-calculus. Information and Computation 81(3), 249–264 (1989)
Vardi, M.Y.: A temporal fixpoint calculus. In: Proc. Conf. on Principles of Programming Languages, POPL 1988, pp. 250–259. ACM Press, New York (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dax, C., Hofmann, M., Lange, M. (2006). A Proof System for the Linear Time μ-Calculus. In: Arun-Kumar, S., Garg, N. (eds) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2006. Lecture Notes in Computer Science, vol 4337. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11944836_26
Download citation
DOI: https://doi.org/10.1007/11944836_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-49994-7
Online ISBN: 978-3-540-49995-4
eBook Packages: Computer ScienceComputer Science (R0)