Abstract
Among the branching-time temporal logics used for the specification and verification of systems, CTL+, FCTL and ECTL+ are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is ΔStackp stack2-complete.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Informatica, 20:207–226, 1983.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Logics of Programs Workshop, Yorktown Heights, New York, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer, 1981.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
S. Demri and Ph. Schnoebelen. The complexity of propositional linear temporal logics in simple cases (extended abstract). In Proc. 15th Ann. Symp. Theoretical Aspects of Computer Science (STACS’98), Paris, France, Feb. 1998, volume 1373 of Lecture Notes in Computer Science, pages 61–72. Springer, 1998.
E. A. Emerson and E. M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Proc. 7th Coll. Automata, Languages and Programming (ICALP’80), Noordwijkerhout, NL, Jul. 1980, volume 85 of Lecture Notes in Computer Science, pages 169–181. Springer, 1980.
E. A. Emerson and J. Y. Halpern. “Sometimes” and “Not Never” revisited: On branching versus linear time. In Proc. 10th ACM Symp. Principles of Programming Languages (POPL’83), Austin, TX, USA, Jan. 1983, pages 127–140, 1983.
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):1–24, 1985.
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.
E. A. Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275–306, 1987.
E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, chapter 16, pages 995–1072. Elsevier Science, 1990.
E. A. Emerson and J. Srinivasan. Branching time temporal logic. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Proc. REX School/Workshop, Noordwijkerhout, NL, May-June 1988, volume 354 of Lecture Notes in Computer Science, pages 123–172. Springer, 1989.
G. Gottlob. NP trees and Carnap’s modal logic. Journal of the ACM, 42(2):421–457, 1995.
M. W. Krentel. The complexity of optimization problems. Journal of Computer and System Sciences, 36(3):490–509, 1988.
L. Lamport. “Sometimes” is sometimes “Not Never”. In Proc. 7th ACM Symp. Principles of Programming Languages (POPL’80), Las Vegas, NV, USA, Jan. 1980, pages 174–185, 1980.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.
H. Ono and A. Nakamura. On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica, 39(4):325–333, 1980.
C. H. Papadimitriou. On the complexity of unique solutions. Journal of the ACM, 31(2):392–400, 1984.
A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS’77), Providence, RI, USA, Oct.-Nov. 1977, pages 46–57, 1977.
A. Rabinovich and Ph. Schnoebelen. BTL 2 and expressive completeness for ECTL +. Research Report LSV-00-8, Lab. Specification and Verification, ENS de Cachan, Cachan, France, October 2000. 21 pages.
A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733–749, 1985.
L. J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1–22, 1976.
K. W. Wagner. More complicated questions about maxima and minima, and some closures of NP. Theoretical Computer Science, 51(1-2):53–80, 1987.
T. Wilke. CTL+ is exponentially more succint than CTL. In Proc. 19th Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS’99), Chennai, India, Dec. 1999, volume 1738 of Lecture Notes in Computer Science, pages 110–121. Springer, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laroussinie, F., Markey, N., Schnoebelen, P. (2001). Model Checking CTL+ and FCTL Is Hard. In: Honsell, F., Miculan, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2001. Lecture Notes in Computer Science, vol 2030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45315-6_21
Download citation
DOI: https://doi.org/10.1007/3-540-45315-6_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41864-1
Online ISBN: 978-3-540-45315-4
eBook Packages: Springer Book Archive