Abstract
In a seminal paper from 1985, Sistla and Clarke showed that satisfiability for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used . If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper undertakes a systematic study of satisfiability for LTL formulae over restricted sets of propositional and temporal operators. Since every propositional operator corresponds to a Boolean function, there exist infinitely many propositional operators. In order to systematically cover all possible sets of them, we use Post’s lattice. With its help, we determine the computational complexity of LTL satisfiability for all combinations of temporal operators and all but two classes of propositional functions. Each of these infinitely many problems is shown to be either PSPACE-complete, NP-complete, or in P.
Keywords: computational complexity, linear temporal logic.
Chapter PDF
Similar content being viewed by others
References
Böhler, E., et al.: Playing with Boolean blocks, part I: Post’s lattice with applications to complexity theory. SIGACT News 34(4), 38–52 (2003)
Bauland, M., et al.: Generalized modal satisfiability. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 500–511. Springer, Heidelberg (2006)
Bauland, M., et al.: The complexity of generalized satisfiability for linear temporal logic. Technical Report TR06-153, Electronic Colloquium on Computational Complexity (2006)
Cook, S.A.: The complexity of theorem proving procedures. In: Proceedings 3rd Symposium on Theory of Computing, pp. 151–158. ACM Press, New York (1971)
Dalmau, V.: Computational Complexity of Problems over Generalized Formulas. PhD thesis, Department de Llenguatges i Sistemes Informàtica, Universitat Politécnica de Catalunya (2000)
Lewis, H.: Satisfiability problems for propositional calculi. Mathematical Systems Theory 13, 45–53 (1979)
Nordh, G.: A trichotomy in the complexity of propositional circumscription. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 257–269. Springer, Heidelberg (2005)
Pippenger, N.: Theories of Computability. Cambridge University Press, Cambridge (1997)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)
Post, E.: The two-valued iterative systems of mathematical logic. Annals of Mathematical Studies 5, 1–122 (1941)
Reith, S.: Generalized Satisfiability Problems. PhD thesis, Fachbereich Mathematik und Informatik, Universität Würzburg (2001)
Reith, S., Vollmer, H.: Optimal satisfiability for propositional calculi and constraint satisfaction problems. Information and Computation 186(1), 1–19 (2003)
Reith, S., Wagner, K.W.: The complexity of problems defined by Boolean circuits. In: Proceedings International Conference Mathematical Foundation of Informatics (MFI99), World Scientific, Singapore (2005)
Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3), 733–749 (1985)
Schnoor, H.: The complexity of the Boolean formula value problem. Technical report, Theoretical Computer Science, University of Hannover (2005)
Stockmeyer, L.: The polynomial-time hierarchy. Theoretical Computer Science 3, 1–22 (1977)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Bauland, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H. (2007). The Complexity of Generalized Satisfiability for Linear Temporal Logic . In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)