The Complexity of Clausal Fragments of LTL
Logic in Computer Science
2013-10-11 v4 Computational Complexity
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.
Keywords
Cite
@article{arxiv.1306.5088,
title = {The Complexity of Clausal Fragments of LTL},
author = {A. Artale and R. Kontchakov and V. Ryzhikov and M. Zakharyaschev},
journal= {arXiv preprint arXiv:1306.5088},
year = {2013}
}
Comments
arXiv admin note: text overlap with arXiv:1209.5571