The Complexity of Clausal Fragments of LTL
A. Artale, R. Kontchakov, V. Ryzhikov, M. Zakharyaschev
TL;DR
This paper explores various fragments of propositional linear temporal logic (LTL), analyzing their computational complexity for satisfiability, revealing a spectrum from low to high complexity classes.
Contribution
It systematically classifies the satisfiability complexity of different LTL fragments based on their operators and clause structures, providing a comprehensive complexity landscape.
Findings
Complexity ranges from NLogSpace to PTime, NP, and PSpace.
Certain fragments are computationally more tractable than others.
The results guide the selection of LTL fragments for practical applications.
Abstract
We introduce and investigate a number of fragments of propo- sitional temporal logic LTL over the flow of time (Z, <). The fragments are defined in terms of the available temporal operators and the structure of the clausal normal form of the temporal formulas. We determine the computational complexity of the satisfiability problem for each of the fragments, which ranges from NLogSpace to PTime, NP and PSpace.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Semantic Web and Ontologies