Details
| Original language | English |
|---|---|
| Title of host publication | Foundations of Software Science and Computational Structures - 10th International Conference, FOSSACS 2007. Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 |
| Publisher | Springer Verlag |
| Pages | 48-62 |
| Number of pages | 15 |
| ISBN (print) | 3540713883, 9783540713883 |
| Publication status | Published - 2007 |
| Event | 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007 - Braga, Portugal Duration: 24 Mar 2007 → 1 Apr 2007 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 4423 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (electronic) | 1611-3349 |
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.
Keywords
- Computational complexity, Linear temporal logic
ASJC Scopus subject areas
- Mathematics(all)
- Theoretical Computer Science
- Computer Science(all)
- General Computer Science
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
Foundations of Software Science and Computational Structures - 10th International Conference, FOSSACS 2007. Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007. Springer Verlag, 2007. p. 48-62 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4423 LNCS).
Research output: Chapter in book/report/conference proceeding › Conference contribution › Research › 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.
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.
KW - Computational complexity
KW - Linear temporal logic
UR - http://www.scopus.com/inward/record.url?scp=37149046257&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-71389-0_5
DO - 10.1007/978-3-540-71389-0_5
M3 - Conference contribution
AN - SCOPUS:37149046257
SN - 3540713883
SN - 9783540713883
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 48
EP - 62
BT - Foundations of Software Science and Computational Structures - 10th International Conference, FOSSACS 2007. Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007
PB - Springer Verlag
T2 - 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007
Y2 - 24 March 2007 through 1 April 2007
ER -