Abstract.
We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that “past is for free”, in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur, R., Henzinger, T.A. (1989) A really temporal logic. Proc. 30th IEEE Symp. Foundations of Computer Science (FOCS’89), Research Triangle Park, NC, USA, pp. 164-169
Alur, R., Henzinger, T.A. (1993) Real-time logics: Complexity and expressiveness. Information and Computation 104(1): 35-77
Benedetti, M., Cimati, A. (2003) Bounded model checking for past LTL. Proc. 9th Int. Conf. Tools and Algorithms for Construction and Analysis of Systems (TACAS’2003) Warsaw, Poland, vol. 2619 (Lecture Notes in Computer Science), pp. 18-33. Springer, Berlin Heidelberg New York
Buss, S.R. (1993) Algorithms for boolean formula evaluation and for tree contraction. In: Clote, P., Krajícek, J. (eds.) Arithmetic, Proof Theory and Computational Complexity, pp. 95-115. Oxford University Press
Clarke, E.M., Emerson, E.A. (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. Proc. Logics of Programs Workshop, Yorktown Heights, New York, vol. 131 (Lecture Notes in Computer Science), pp. 52-71. Springer, Berlin Heidelberg New York
Clarke, E.M., Emerson, E.A., Sistla, A.P. (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2): 244-263
Clarke, E.M., Grumberg, O., Peled, D.A. (1999) Model Checking. MIT Press
Demri, S., Schnoebelen, Ph. (2002) The complexity of propositional linear temporal logics in simple cases. Information and Computation 174(1): 84-103
Emerson, E.A. (1990) Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, chapter 16, pp. 995-1072. Elsevier Science
Etessami, K., Vardi, M.Y., Wilke, T. (1997) First order logic with two variables and unary temporal logic. Proc. 12th IEEE Symp. Logic in Computer Science (LICS’97), Warsaw, Poland, pp. 228-235. IEEE Comp. Soc. Press
Gabbay, D.M. (1987) The declarative past and imperative future: Executable temporal logic for interactive systems. Proc. Workshop Temporal Logic in Specification, Altrincham, UK, vol. 398 (Lecture Notes in Computer Science), pp. 409-448. Springer, Berlin Heidelberg New York
Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J. (1980) On the temporal analysis of fairness. Proc. 7th ACM Symp. Principles of Programming Languages (POPL’80), Las Vegas, NV, USA, pp. 163-173
Gastin, P., Oddoux, D. (2003) LTL with past and two-way very-weak alternating automata. Proc. 28th Int. Symp. Mathematical Foundations of Computer Science (MFCS 2003), Bratislava, Slovak Republic, vol. 2747 (Lecture Notes in Computer Science), pp. 439-448. Springer, Berlin Heidelberg New York
Harel, D. (1983) Recurring dominos: Making the highly undecidable highly understandable. Annals of Discrete Mathematics 24: 51-72
Kamp, J.A.W. (1968) Tense Logic and the Theory of Linear Order. PhD thesis, UCLA, Los Angeles, CA, USA
Kesten, Y., Manna, Z., McGuire, H., Pnueli, A. (1993) A decision algorithm for full propositional temporal logic. Proc. 5th Int. Conf. Computer Aided Verification (CAV’93), Elounda, Greece, vol. 697 (Lecture Notes in Computer Science), pp. 97-109. Springer, Berlin Heidelberg New York
Koymans, R. (1990) Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4): 255-299
Kupferman, O., Pnueli, A. (1995) Once and for all. Proc. 10th IEEE Symp. Logic in Computer Science (LICS’95), San Diego, CA, USA, pp. 25-35. IEEE Comp. Soc. Press
Laroussinie, F., Markey, N., Schnoebelen, Ph. (2001) Model checking CTL+ and FCTL is hard. Proc. 4th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS’2001), Genoa, Italy, vol. 2030 (Lecture Notes in Computer Science), pp. 318-331. Springer, Berlin Heidelberg New York
Laroussinie, F., Markey, N., Schnoebelen, Ph. (2002) On model checking durational Kripke structures (extended abstract). Proc. 5th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS’2002), Grenoble, France, vol. 2303 (Lecture Notes in Computer Science), pp. 264-279. Springer, Berlin Heidelberg New York
Laroussinie, F., Markey, N., Schnoebelen, Ph. (2002) Temporal logic with forgettable past. Proc. 17th IEEE Symp. Logic in Computer Science (LICS’2002), Copenhagen, Denmark, pp. 383-392. IEEE Comp. Soc. Press
Laroussinie, F., Schnoebelen, Ph. (1995) A hierarchy of temporal logics with past. Theoretical Computer Science 148(2): 303-324
Lichtenstein, O., Pnueli, A., Zuck, L.D. (1985) The glory of the past. Proc. Logics of Programs Workshop, Brooklyn, NY, USA, vol. 193 (Lecture Notes in Computer Science), pp. 196-218. Springer, Berlin Heidelberg New York
Manna, Z., Pnueli, A. (1991) Completing the temporal picture. Theoretical Computer Science 83: 97-130
Manna, Z., Pnueli, A. (1992) The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin Heidelberg New York
Manna, Z., Pnueli, A. (1995) Temporal Verification of Reactive Systems: Safety. Springer, Berlin Heidelberg New York
Markey, N. (2003) Temporal logic with past is exponentially more succinct. EATCS Bull. 79: 122-128
Markey, N., Schnoebelen, Ph. (2003) Model checking a path (preliminary report). Proc. 14th Int. Conf. Concurrency Theory (CONCUR 2003), Marseilles, France, vol. 2761 (Lecture Notes in Computer Science), pp. 251-265. Springer, Berlin Heidelberg New York
Pnueli, A. (1977) The temporal logic of programs. Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS’77), Providence, RI, USA, pp. 46-57
Ramakrishna, Y.S., Moser, L.E., Dillon, L.K., Melliar-Smith, P.M., Kutty, G. (1992) An automata-theoretic decision procedure for propositional temporal logic with Since and Until. Fundamenta Informaticae 17(3): 271-282
Schnoebelen, Ph. (2003) Oracle circuits for branching-time model checking. Proc. 30th Int. Coll. Automata, Languages, and Programming (ICALP’2003), Eindhoven, NL, vol. 2719 (Lecture Notes in Computer Science), pp. 790-801. Springer, Berlin Heidelberg New York
Sistla, A.P., Clarke, E.M. (1985) The complexity of propositional linear temporal logics. Journal of the ACM 32(3): 733-749
Vardi, M.Y., Wolper, P. (1994) Reasoning about infinite computations. Information and Computation 115(1): 1-37
Author information
Authors and Affiliations
Corresponding author
Additional information
Received: 4 September 2002, Published online: 17 March 2004
Rights and permissions
About this article
Cite this article
Markey, N. Past is for free: on the complexity of verifying linear temporal properties with past. Acta Informatica 40, 431–458 (2004). https://doi.org/10.1007/s00236-003-0136-5
Issue Date:
DOI: https://doi.org/10.1007/s00236-003-0136-5