Abstract
It is proved that CTL+ is exponentially more succinct than CTL. More p recisely, it is shown that every CTL formula (and every modal μ-calculus formula) equivalent to the CTL+ formula E(Fp 0 ∧ · · · ∧ Fpn—1) is of length at least ( n⌈n/2⌉ ), which is \( \Omega (2^n /\sqrt n )\) . This matches almost the upper bound provided by Emerson and Halpern, which says that for every CTL+ formula of length n there exists an equivalent CTL formula of length at most 2n log n.
It follows that the exponential blow-up as incurred in known conversions of nondeterministic Büchi word automata into alternation-free μ-calculus formulas is unavoidable. This answers a question posed by Kupferman and Vardi.
The proof of the above lower bound exploits the fact that for every CTL (μ-calculus) formula there exists an equivalent alternating tree automaton of linear size. The core of this proof is an involved cut-and-paste argument for alternating tree automata.
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
O. Bernholtz [Kupferman] and O. Grumberg. Branching temporal logic and amorphous tree automata. In E. Best, ed., CONCUR’93, vol. 715 of LNCS, 262–277. 111
O. Bernholtz [Kupferman], M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In D. L. Dill, ed., CAV’ 94, vol. 818 of LNCS, 142–155. 111, 115, 116, 116, 119
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications: A practical approach. In PoPL’ 83, 117–126. 111
E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. In STOC’ 82, 169–181. 110, 111, 111
E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. System Sci., 30(1):1–24, 1985. 110, 111, 111, 113
E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model-checking for fragments of µ-calculus. In C. Courcoubetis, ed., CAV’ 93, vol. 697 of LNCS, 385–396. 111
E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In LICS’ 86, 267–278. 120
K. Etessami, M. Y. Vardi, and Th. Wilke. First-order logic with two variables and unary temporal logic. In LICS’ 97, 228–235. 111, 111
J. A. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, Calif., 1968. 110
O. Kupferman and M. Y. Vardi. Freedom, weakness, and determinism: From linear-time to branching-time. In LICS’ 98, 81–92. 111, 111, 120, 120
L. J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, Dept. of Electrical Engineering, MIT, Boston, Mass., 1974. 110
Th. Wilke. CTL + is exponentially more succinct than CTL. Technical Report 99-7, RWTH Aachen, Fachgruppe Informatik, 1999. Available online via ftp://ftp.informatik.rwth-aachen.de/pub/reports/1999/index.html. 112
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wilke, T. (1999). CTL+ Is Exponentially More Succinct than CTL. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1999. Lecture Notes in Computer Science, vol 1738. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46691-6_9
Download citation
DOI: https://doi.org/10.1007/3-540-46691-6_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66836-7
Online ISBN: 978-3-540-46691-8
eBook Packages: Springer Book Archive