The Complexity of Satisfiability for Fragments of CTL and CTL⋆

Show simple item record

dc.identifier.uri http://dx.doi.org/10.15488/1518
dc.identifier.uri http://www.repo.uni-hannover.de/handle/123456789/1543
dc.contributor.author Meier, Arne
dc.contributor.author Mundhenk, Martin
dc.contributor.author Thomas, Michael
dc.contributor.author Vollmer, Heribert
dc.date.accessioned 2017-05-11T07:53:37Z
dc.date.available 2017-05-11T07:53:37Z
dc.date.issued 2008
dc.identifier.citation Meier, Arne; Mundhenk, M.; Thomas, Michael; Vollmer, Heribert: The Complexity of Satisfiability for Fragments of CTL and CTL⋆. In: Electronic Notes in Theoretical Computer Science 223 (2008), Nr. C, S. 201-213. DOI: https://doi.org/10.1016/j.entcs.2008.12.040
dc.description.abstract The satisfiability problems for CTL and CTL⋆ are known to be EXPTIME-complete, resp. 2EXPTIME-complete (Fischer and Ladner (1979), Vardi and Stockmeyer (1985)). For fragments that use less temporal or propositional operators, the complexity may decrease. This paper undertakes a systematic study of satisfiability for CTL- and CTL⋆-formulae over restricted sets of propositional and temporal operators. We show that restricting the temporal operators yields satisfiability problems complete for 2EXPTIME, EXPTIME, PSPACE, and NP. Restricting the propositional operators either does not change the complexity (as determined by the temporal operators), or yields very low complexity like NC1, TC0, or NLOGTIME. eng
dc.language.iso eng
dc.publisher Amsterdam : Elsevier BV
dc.relation.ispartofseries Electronic Notes in Theoretical Computer Science 223 (2008), Nr. C
dc.rights CC BY-NC-ND 3.0
dc.rights.uri https://creativecommons.org/licenses/by-nc-nd/3.0/
dc.subject Post's Lattice eng
dc.subject Satisfiability eng
dc.subject Temporal Logic eng
dc.subject Real time systems eng
dc.subject Post's Lattice eng
dc.subject Satisfiability eng
dc.subject Satisfiability problems eng
dc.subject Systematic studies eng
dc.subject Temporal operators eng
dc.subject Very low complexities eng
dc.subject Temporal logic eng
dc.subject.ddc 004 | Informatik ger
dc.title The Complexity of Satisfiability for Fragments of CTL and CTL⋆
dc.type article
dc.type Text
dc.relation.issn 1571-0661
dc.relation.doi https://doi.org/10.1016/j.entcs.2008.12.040
dc.bibliographicCitation.issue C
dc.bibliographicCitation.volume 223
dc.bibliographicCitation.firstPage 201
dc.bibliographicCitation.lastPage 213
dc.description.version publishedVersion
tib.accessRights frei zug�nglich


Files in this item

This item appears in the following Collection(s):

Show simple item record

 

Search the repository


Browse

My Account

Usage Statistics