| |
VOLUME 5, ISSUE 1, PAPER 1
|
The Complexity of Generalized Satisfiability for Linear Temporal Logic
|
©Michael Bauland, Knipp GmbH, Deutschland
©Thomas Schneider, University of Manchester, UK
©Henning Schnoor, Rochester Institute of Technology, USA
©Ilka Schnoor, Rochester Institute of Technology, USA
©Heribert Vollmer, University of Hannover, Germany
|
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.
|
Publication date: January 26, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(1:1)2009
Hit Counts: 1674 |
 Creative Commons | |
