Augmenting branching temporal logics with existential quantification over atomic propositions
Copyright policy )Augmenting branching temporal logics with existential quantification over atomic propositions
Temporal-logic model checking is used in verification of program correctness. The complexity of model-checking algorithms on finite propositional Kripke structures was established previously, in particular for the temporal logics CTL and CTL*. The author explores the relevant complexities when we enrich CTL and CTL* by existential quantification over atomic propositions. By this enrichment, the structure semantics and the (unfolded) computation tree semantics differ. This yields four cases to examine. Besides the complexity of the model checking problem (where the instance is a finite-state program and a formula), the author also studies, in each of the four cases, the so-called program complexity (when the formula is fixed). Therefore the paper contains eight complexity results, varying from P-completeness to 2EXPTIME-completeness.
- Technion – Israel Institute of Technology Israel
- University of California, Berkeley United States
Specification and verification (program logics, model checking, etc.), Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), Temporal logic, branching temporal logics, complexity, model checking, program complexity
Specification and verification (program logics, model checking, etc.), Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), Temporal logic, branching temporal logics, complexity, model checking, program complexity
selected citations These citations are derived from selected sources.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).20 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.Average 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.Average
Citations provided by BIP!Popularity provided by BIP!