A fragment of linear time temporal logic (LTL) is presented. It is proved that the satisfiability problem for this fragment is NP-complete. The fragment is larger than previously known NP-complete fragments. It is obtained by prohibiting the use of until operator and requiring to use only next operators indexed by a letter. © Springer-Verlag Berlin Heidelberg 2004.
CITATION STYLE
Muscholl, A., & Walukiewicz, I. (2004). An NP-complete fragment of LTL. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3340, 334–344. https://doi.org/10.1007/978-3-540-30550-7_28
Mendeley helps you to discover research relevant for your work.