THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
Copyright policy )THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
The satisfiability problems for [Formula: see text] and [Formula: see text] 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 [Formula: see text]-and [Formula: see text]-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.
- Friedrich Schiller University Jena Germany
- University of Hannover Germany
- Schiller International University France
Post's Lattice, Real time systems, Very low complexities, Temporal logic, Theoretical Computer Science, Satisfiability problems, Dewey Decimal Classification::000 | Allgemeines, Wissenschaft::000 | Informatik, Wissen, Systeme::004 | Informatik, Temporal Logic, Systematic studies, Temporal operators, Satisfiability, Computer Science(all)
Post's Lattice, Real time systems, Very low complexities, Temporal logic, Theoretical Computer Science, Satisfiability problems, Dewey Decimal Classification::000 | Allgemeines, Wissenschaft::000 | Informatik, Wissen, Systeme::004 | Informatik, Temporal Logic, Systematic studies, Temporal operators, Satisfiability, Computer Science(all)
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).24 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!