Abstract
We investigate the complexity of satisfiability and finite-state model-checking problems for the branching-time logic CTL\(^*_{lp}\), an extension of CTL* with past-time operators, where past is linear, finite, and cumulative. It is well-known that CTL\(^*_{lp}\) has the same expressiveness as standard CTL*, but the translation of CTL\(^*_{lp}\) into CTL* is of non-elementary complexity, and no elementary upper bounds are known for its satisfiability and finite-state model checking problems. In this paper, we provide an elegant and uniform framework to solve these problems, which non-trivially extends the standard automata-theoretic approach to CTL* model-checking. In particular, we show that the satisfiability problem for CTL\(^*_{lp}\) is 2Exptime-complete, which is the same complexity as that of CTL*, but for the existential fragment of CTL\(^*_{lp}\), the problem is Expspace-complete, hence exponentially harder than that of the existential fragment of CTL*. For the model-checking, the problem is already Expspace-complete for the existential and universal fragments of CTL\(^*_{lp}\). For full CTL\(^*_{lp}\), the proposed algorithm runs in time polynomial in the size of the Kripke structure and doubly exponential in the size of the formula. Thus, the exact complexity of model-checking full CTL\(^*_{lp}\) remains open: it lies somewhere between Expspace and 2Exptime.
Chapter PDF
References
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: On branching versus linear time. Journal of the ACM 33(1), 151–178 (1986)
Hafer, T., Thomas, W.: Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 269–279. Springer, Heidelberg (1987)
Kupferman, O., Pnueli, A.: Once and For All. In: Proc. 10th LICS, pp. 25–35. IEEE Comp. Soc. Press, Los Alamitos (1995)
Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Proc. 30th STOC, pp. 224–233. ACM, New York (1998)
Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to modular model checking. ACM Trans. Program. Lang. Syst. 22(1), 87–128 (2000)
Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proc. 21th LICS, pp. 265–274. IEEE Comp. Soc. Press, Los Alamitos (2006)
Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking. J. ACM 47(2), 312–360 (2000)
Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theoretical Computer Science 148(2), 303–324 (1995)
Laroussinie, F., Schnoebelen, P.: Specification in CTL+past for verification in CTL. Information and Computation 156(1–2), 236–263 (2000)
Muller, D.E., Schupp, P.E.: Alternating Automata on Infinite Trees. Theoretical Computer Science 54, 267–276 (1987)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)
Pistore, M., Vardi, M.Y.: The planning spectrum - one, two, three, infinity. In: Proc. 18th LICS, pp. 234–243. IEEE Comp. Soc. Press, Los Alamitos (2003)
Vardi, M.Y.: A temporal fixpoint calculus. In: Proc. 15th Annual POPL, pp. 250–259. ACM, New York (1988)
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)
Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: Proc. 17th STOC, pp. 240–251 (1985)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Wilke, T.: CTL + is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 110–121. Springer, Heidelberg (1999)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1–2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozzelli, L. (2008). The Complexity of CTL* + Linear Past. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)