The complexity of propositional linear temporal logics

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The complexity of propositional linear temporal logics

Full text

Pdf (1.46 MB)

Source

Journal of the ACM (JACM) archive
Volume 32 , Issue 3 (July 1985) table of contents

Pages: 733 - 749

Year of Publication: 1985

ISSN:0004-5411

Authors

A. P. Sistla	Univ. of Massachusetts, Amherst
E. M. Clarke	Carnegie-Mellon Univ., Pittsburgh, PA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 144, Citation Count: 85

Additional Information:

abstract references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/3828.3837 What is a DOI?

ABSTRACT

The complexity of satisfiability and determination of truth in a particular finite structure are considered for different propositional linear temporal logics. It is shown that these problems are NP-complete for the logic with F and are PSPACE-complete for the logics with F, X, with U, with U, S, X operators and for the extended logic with regular operators given by Wolper.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
	2	HALPERN, J. Y., AND REIF, J. H.The propositional dynamic logic of deterministic, well-structured programs. In Proceedings of the 22nd Symposium on Foundations of Computer Science (Nashville, Tenn.) IEEE, New York, 1981, pp. 322-334. Also in Theoret. Comput. Sci., 27 (1983), 127-165.
	3	LADNER, R. The computational complexity of provabiiity in systems of modal propositional logic. SlAM J. Comput. 6 (1977), 467-480.
	4	ONO, H. AND NAKAMURA, A.On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica 39 (1980), 325-333.
	5	Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, Logic of Programs, Workshop, p.253-281, May 01, 1981
	6	PNUELI, A.The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (Providence, R.I.). IEEE, New York, 1977, pp. 46-57.
	7	Edward L. Robertson, Structure of complexity in the weak monadic second-order theories of the natural numbers, Proceedings of the sixth annual ACM symposium on Theory of computing, p.161-171, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803895]
	8	SAVITCH, W.J. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 2 (1970), 177-192.
	9	A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.159-168, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802189]
	10	WOLPER, P.Temporal logic can be more expressive. In Proceedings of 22nd Symposium on Foundations of Computer .Science (Nashville, Tenn.). IEEE, New York, !98 !, pp. 340-348. Also in Inf. Control 56 (1983), 72-99.

CITED BY 85

	Jan Chomicki , Damian Niwiński, On the feasibility of checking temporal integrity constraints, Proceedings of the twelfth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.202-213, May 25-28, 1993, Washington, D.C., United States
	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986
	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States
	Rainer Schlör , Franz Korf, Verification of a production cell controller using symbolic timing diagrams, Proceedings of the conference on European design automation, p.548-553, September 18-22, 1995, Brighton, England
	P. Y. Schobbens , G. Saake , A. Sernadas , C. Sernadas, A two-level temporal logic for evolving specifications, Information Processing Letters, v.83 n.3, p.167-172, 16 August 2002
	Steven M. German , A. Prasad Sistla, Reasoning about systems with many processes, Journal of the ACM (JACM), v.39 n.3, p.675-735, July 1992
	Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996
	M. Y. Vardi, A temporal fixpoint calculus, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-259, January 10-13, 1988, San Diego, California, United States
	R. P. Kurshan, The complexity of verification, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.365-371, May 23-25, 1994, Montreal, Quebec, Canada
	Joanne Atlee , John Gannon, State-based model checking of event-driven system requirements, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.16-28, Dec. 1991
	Jan Chomicki , Tomasz Imieliński, Temporal deductive databases and infinite objects, Proceedings of the seventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.61-73, March 1988, Austin, Texas, United States
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	S. Safra , M. Y. Vardi, On &ohgr;-automata and temporal logic, Proceedings of the twenty-first annual ACM symposium on Theory of computing, p.127-137, May 14-17, 1989, Seattle, Washington, United States
	Ronald Fagin , Yoram Moses , Joseph Y. Halpern , Moshe Y. Vardi, Knowledge-based programs, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.153-163, August 20-23, 1995, Ottowa, Ontario, Canada
	Joseph Halpern , Vardi, Reasoning about knowledge and time in asynchronous systems, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.53-65, May 02-04, 1988, Chicago, Illinois, United States
	E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986
	Costas Courcoubetis , Mihalis Yannakakis, The complexity of probabilistic verification, Journal of the ACM (JACM), v.42 n.4, p.857-907, July 1995
	Stéphane Demri , Philippe Schnoebelen, The complexity of propositional linear temporal logics in simple cases, Information and Computation, v.174 n.1, p.84-103, April 10, 2002
	Michael Fisher , Clare Dixon , Martin Peim, Clausal temporal resolution, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.12-56, Jan. 2001
	E M Clarke , O Grumberg , M C Browne, Reasoning about networks with many identical finite-state processes, Proceedings of the fifth annual ACM symposium on Principles of distributed computing, p.240-248, August 11-13, 1986, Calgary, Alberta, Canada
	Iain A. Stewart, The complexity of achievement and maintenance problems in agent-based systems, Artificial Intelligence, v.146 n.2, p.175-191, June 2003
	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994
	E. M. Clarke , O. Grumberg, Avoiding the state explosion problem in temporal logic model checking, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.294-303, August 10-12, 1987, Vancouver, British Columbia, Canada
	Miguel J. Hornos , Manuel I. Capel, On-the-fly model checking from interval logic specifications, ACM SIGPLAN Notices, v.37 n.12, December 2002
	Orna Kupferman , Moshe Y. Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.87-128, Jan. 2000
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Martín Abadi , Zohar Manna, Nonclausal deduction in first-order temporal logic, Journal of the ACM (JACM), v.37 n.2, p.279-317, April 1990
	Oliver Kutz , Carsten Lutz , Frank Wolter , Michael Zakharyaschev, ε-connections of abstract description systems, Artificial Intelligence, v.156 n.1, p.1-73, June 2004
	Reiner Hähnle, Complexity of many-valued logics, Beyond two: theory and applications of multiple-valued logic, Physica-Verlag GmbH, Heidelberg, Germany, 2003
	Marc Spielmann, Verification of relational transducers for electronic commerce, Journal of Computer and System Sciences, v.66 n.1, p.40-65, 01 February 2003
	M. Reynolds, The complexity of the temporal logic with "until" over general linear time, Journal of Computer and System Sciences, v.66 n.2, p.393-426, March 2003
	Michael Dekhtyar , Alexander Dikovsky , Mars Valiev, On feasible cases of checking multi-agent systems behavior, Theoretical Computer Science, v.303 n.1, p.63-81, 28 June 2003
	Rajeev Alur , Salvatore La Torre, Deterministic generators and games for Ltl fragments, ACM Transactions on Computational Logic (TOCL), v.5 n.1, p.1-25, January 2004
	Kousha Etessami , Moshe Y. Vardi , Thomas Wilke, First-order logic with two variables and unary temporal logic, Information and Computation, v.179 n.2, p.279-295, December 15, 2002
	Rajeev Alur , Thomas A. Henzinger, A really temporal logic, Journal of the ACM (JACM), v.41 n.1, p.181-203, Jan. 1994
	J Y Halpern , M Y Vardi, The complexity of reasoning about knowledge and time, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.304-315, May 28-30, 1986, Berkeley, California, United States
	Krishnendu Chatterjee , Pallab Dasgupta , P. P. Chakrabarti, The power of first-order quantification over states in branching and linear time temporal logics, Information Processing Letters, v.91 n.5, p.201-210, 15 September 2004
	Olivier Serre, Vectorial languages and linear temporal logic, Theoretical Computer Science, v.310 n.1-3, p.79-116, 01 January 2004
	V. K. Garg , B. Waldecker, Detection of Weak Unstable Predicates in Distributed Programs, IEEE Transactions on Parallel and Distributed Systems, v.5 n.3, p.299-307, March 1994
	Moshe Y. Vardi, Implementing knowledge-based programs, Proceedings of the 6th conference on Theoretical aspects of rationality and knowledge, March 17-20, 1996, The Netherlands
	Edith Spaan, Nexttime is not necessary, Proceedings of the 3rd conference on Theoretical aspects of reasoning about knowledge, March 04-07, 1990, Pacific Grove, California
	Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
	Ronald Fagin , Joseph Y. Halpern , Yoram Moses , Moshe Y. Vardi, Knowledge-based programs, Distributed Computing, v.10 n.4, p.199-225, July 1997
	Frank Wolter , Michael Zakharyaschev, Qualitative spatiotemporal representation and reasoning: a computational perspective, Exploring artificial intelligence in the new millennium, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
	Karl Krukow , Mogens Nielsen , Vladimiro Sassone, A framework for concrete reputation-systems with applications to history-based access control, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA
	Anssi Yli-Jyrä, Describing syntax with star-free regular expressions, Proceedings of the tenth conference on European chapter of the Association for Computational Linguistics, April 12-17, 2003, Budapest, Hungary
	Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, v.10 n.1, p.47-71, February 1997
	Pierre Wolper, Expressing interesting properties of programs in propositional temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.184-193, January 01, 1986, St. Petersburg Beach, Florida
	F. Laroussinie , N. Markey , Ph. Schnoebelen, Efficient timed model checking for discrete-time systems, Theoretical Computer Science, v.353 n.1, p.249-271, 14 March 2006
	S. Demri , F. Laroussinie , Ph. Schnoebelen, A parametric analysis of the state-explosion problem in model checking, Journal of Computer and System Sciences, v.72 n.4, p.547-575, June 2006
	Alexander Rabinovich , Philippe Schnoebelen, BTL2 and the expressive power of ECTL⁺, Information and Computation, v.204 n.7, p.1023-1044, July 2006
	Mark Lawford , Vera Pantelic , Hong Zhang, Towards integrated verification of timed transition models, Fundamenta Informaticae, v.70 n.1, p.75-110, March 2006
	A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States
	Stéphane Demri, LTL Over integer periodicity constraints, Theoretical Computer Science, v.360 n.1, p.96-123, 21 August 2006
	Stéphane Demri , Deepak D'Souza, An automata-theoretic approach to constraint LTL, Information and Computation, v.205 n.3, p.380-415, March, 2007
	Carsten Lutz , Dirk Walther , Frank Wolter, Quantitative temporal logics over the reals: PSpace and below, Information and Computation, v.205 n.1, p.99-123, January, 2007
	Stéphane Demri , Ranko Lazić , David Nowak, On the freeze quantifier in Constraint LTL: Decidability and complexity, Information and Computation, v.205 n.1, p.2-24, January, 2007
	Thomas Ågotnes , Wiebe van der Hoek , Michael Wooldridge, Temporal qualitative coalitional games, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
	Laura Bozzelli, Complexity results on branching-time pushdown model checking, Theoretical Computer Science, v.379 n.1-2, p.286-297, June, 2007
	Laura Giordano , Alberto Martelli, Tableau-based automata construction for dynamic linear time temporal logic*, Annals of Mathematics and Artificial Intelligence, v.46 n.3, p.289-315, March 2006
	I. P. de Guzmán , M. Ojeda-Aciego , A. Valverde, Implicates and reduction techniques for temporal logics, Annals of Mathematics and Artificial Intelligence, v.27 n.1-4, p.3-23, 1999
	Michael Wooldridge , Paul E. Dunne, The complexity of agent design problems: Determinism and history dependence, Annals of Mathematics and Artificial Intelligence, v.45 n.3-4, p.343-371, December 2005
	Joel Richardson, Supporting Lists in a Data Model (A Timely Approach), Proceedings of the 18th International Conference on Very Large Data Bases, p.127-138, August 23-27, 1992
	A. N. Chebotarev, The Automata-Theoretic Approach to Verification of Reactive Systems, Cybernetics and Systems Analysis, v.37 n.6, p.810-819, November-December 2001
	A. N. Chebotarev, Construction of an Automaton From a Formula of the Monadic First-Order Theory of Natural Numbers, Cybernetics and Systems Analysis, v.37 n.4, p.540-550, July-August 2001
	Grigore Roşu , Klaus Havelund, Rewriting-Based Techniques for Runtime Verification, Automated Software Engineering, v.12 n.2, p.151-197, April 2005
	Igor Walukiewicz, Difficult Configurations—On the Complexity of LTrL, Formal Methods in System Design, v.26 n.1, p.27-43, January 2005
	Brandon Bennett , Anthony G. Cohn , Frank Wolter , Michael Zakharyaschev, Multi-Dimensional Modal Logic as a Framework for Spatio-Temporal Reasoning, Applied Intelligence, v.17 n.3, p.239-251, November-December 2002
	Stéphane Demri , Régis Gascon, Verification of qualitative Z constraints, Theoretical Computer Science, v.409 n.1, p.24-40, December, 2008
	Arne Meier , Martin Mundhenk , Michael Thomas , Heribert Vollmer, The Complexity of Satisfiability for Fragments of CTL and CTL*;, Electronic Notes in Theoretical Computer Science (ENTCS), 223, p.201-213, December, 2008
	Michał Walicki , Marc Bezem , Wojtek Szajnkenig, Developing Bounded Reasoning, Journal of Logic, Language and Information, v.18 n.1, p.97-129, January 2009
	Jeffrey Fischer , Rupak Majumdar, Ensuring consistency in long running transactions, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Tobias Nopper , Christoph Scholl , Bernd Becker, Computation of minimal counterexamples by using black box techniques and symbolic methods, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
	Karl Krukow , Mogens Nielsen , Vladimiro Sassone, A logical framework for history-based access control and reputation systems, Journal of Computer Security, v.16 n.1, p.63-101, January 2008
	Vladimir V. Rybakov, Decidability w.r.t. Logical Consecutions of Linear Temporal Logic Extended by Since and Previous, Fundamenta Informaticae, v.81 n.1-3, p.297-313, January 2007
	Volker Diekert , Martin Horsch , Manfred Kufleitner, On First-Order Fragments for Mazurkiewicz Traces, Fundamenta Informaticae, v.80 n.1-3, p.1-29, January 2007
	Stijn Heymans , Davy Van Nieuwenborgh , Dirk Vermeir, Open answer set programming with guarded programs, ACM Transactions on Computational Logic (TOCL), v.9 n.4, p.1-53, August 2008
	Victor Vianu, Automatic verification of database-driven systems: a new frontier, Proceedings of the 12th International Conference on Database Theory, March 23-25, 2009, St. Petersburg, Russia
	Hana Chockler , Ofer Strichman, Before and after vacuity, Formal Methods in System Design, v.34 n.1, p.37-58, February 2009
	Michael Bauland , Martin Mundhenk , Thomas Schneider , Henning Schnoor , Ilka Schnoor , Heribert Vollmer, The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments, Electronic Notes in Theoretical Computer Science (ENTCS), 231, p.277-292, March, 2009
	Arnab Sinha , Pallab Dasgupta , Bhaskar Pal , Sayantan Das , Prasenjit Basu , P. P. Chakrabarti, Design intent coverage revisited, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.14 n.1, p.1-32, January 2009
	David Gabelaia , Roman Kontchakov , Agi Kurucz , Frank Wolter , Michael Zakharyaschev, Combining spatial and temporal logics: expressiveness vs. complexity, Journal of Artificial Intelligence Research, v.23 n.1, p.167-243, January 2005
	Marco Pistore , Moshe Y. Vardi, The planning spectrum: one, two, three, infinity, Journal of Artificial Intelligence Research, v.30 n.1, p.101-132, September 2007
	Clare Dixon , Michael Fisher , Boris Konev, Tractable temporal reasoning, Proceedings of the 20th international joint conference on Artifical intelligence, p.318-323, January 06-12, 2007, Hyderabad, India

INDEX TERMS

Primary Classification:
F. Theory of Computation
F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
F.2.2 Nonnumerical Algorithms and Problems
Subjects: Complexity of proof procedures

Additional Classification:
F. Theory of Computation
F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
F.4.1 Mathematical Logic
Subjects: Temporal logic

General Terms:
Performance, Theory, Verification

REVIEW

"Gregory E. Minc : Reviewer"

Propositional linear temporal logic deals with the sequence of states 0, 1, 2, and connectives X (true in the next state), F (true in some subsequent state), U (until), and S (since). Its importance derives fr more...

Collaborative Colleagues:

A. P. Sistla: colleagues

E. M. Clarke: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player