It is well-known that model-checking and satisfiability for PLTL are PSPACE-complete. By contrast, very little is known about whether there exist some interesting fragments of PLTL with a lower worst-case complexity. Such results would help understand why PLTL model-checkers are successfully used in practice. In this paper we investigate this issue and consider model-checking and satisfiability for all fragments of PLTL one obtains when restrictions are put on (1) the temporal connectives allowed, (2) the number of atomic propositions, and (3) the temporal height. © 1998 Springer-Verlag.
CITATION STYLE
Demri, S., & Schnoebelen, P. (1998). The complexity of propositional linear temporal logics in simple cases (extended abstract). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1373 LNCS, pp. 61–72). https://doi.org/10.1007/BFb0028549
Mendeley helps you to discover research relevant for your work.