The complexity of generalized satisfiability for linear temporal logic

Michael Bauland; Thomas Schneider; Henning Schnoor; Ilka Schnoor; Heribert Vollmer

The complexity of generalized satisfiability for linear temporal logic

Michael Bauland, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 prepositional 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. © Springer-Verlag Berlin Heidelberg 2007.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Pages	48-62
Number of pages	14
Volume	4423
Publication status	Published - 2007
Event	10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007 - Braga Duration: 1 Jul 2007 → …

Conference

Conference	10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007
City	Braga
Period	1/07/07 → …

Keywords

Computational complexity
Linear temporal logic

Cite this

@inproceedings{0a2de6396971441c8708bb7506f40e71,

title = "The complexity of generalized satisfiability for linear temporal logic",

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 prepositional 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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.",

keywords = "Computational complexity, Linear temporal logic",

author = "Michael Bauland and Thomas Schneider and Henning Schnoor and Ilka Schnoor and Heribert Vollmer",

year = "2007",

language = "English",

isbn = "3540713883",

volume = "4423",

pages = "48--62",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

note = "10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007 ; Conference date: 01-07-2007",

}

Bauland, M, Schneider, T, Schnoor, H, Schnoor, I & Vollmer, H 2007, The complexity of generalized satisfiability for linear temporal logic. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 4423, pp. 48-62, 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007, Braga, 1/07/07.

The complexity of generalized satisfiability for linear temporal logic. / Bauland, Michael; Schneider, Thomas; Schnoor, Henning et al.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 4423 2007. p. 48-62.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - The complexity of generalized satisfiability for linear temporal logic

AU - Bauland, Michael

AU - Schneider, Thomas

AU - Schnoor, Henning

AU - Schnoor, Ilka

AU - Vollmer, Heribert

PY - 2007

Y1 - 2007

N2 - 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 prepositional 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. © Springer-Verlag Berlin Heidelberg 2007.

AB - 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 prepositional 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. © Springer-Verlag Berlin Heidelberg 2007.

KW - Computational complexity

KW - Linear temporal logic

M3 - Conference contribution

SN - 3540713883

SN - 9783540713883

VL - 4423

SP - 48

EP - 62

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

T2 - 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007

Y2 - 1 July 2007

ER -

The complexity of generalized satisfiability for linear temporal logic

Abstract

Conference

Keywords

Fingerprint

Cite this