Logo image
Back
The Complexity of Clausal Fragments of LTL
Conference proceeding   Open access  Peer reviewed

The Complexity of Clausal Fragments of LTL

Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov and Michael Zakharyaschev
Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, Vol.8312, pp.35-52
Lecture Notes in Computer Science, 8312
LPAR-19 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (Stellenbosch, 15/12/2013 - 19/12/2013)
2013
DOI: https://doi.org/10.1007/978-3-642-45221-5_3
Handle:
https://hdl.handle.net/10863/878

Abstract

We introduce and investigate a number of fragments of propositional temporal logic LTL over the flow of time (ℤ, <). 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.
url
http://www.cs.sun.ac.za/lpar-19/View
url
http://link.springer.com/chapter/10.1007/978-3-642-45221-5_3#page-1View

Details

Metrics

35 Record Views