Deadlock boundary of infinite-run CTL*

TheoremNo existential path formula holds at a terminal state#✓fully proved

No existential infinite path formula holds at a terminal state.

theorem not_stateSat_exists_of_terminal (hdead : lts.IsTerminal s) :
    ¬StateSat lts valuation (.exists π) s

Uses 5

Statement usesPath formulas of CTL\(^{\ast}\) · State formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) state formulas

Proof usesSatisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Infinite run

TheoremUniversal path formulas hold vacuously at terminal states#✓fully proved

Universal infinite path quantification is vacuous at a terminal state.

theorem stateSat_forall_of_terminal (hdead : lts.IsTerminal s) :
    StateSat lts valuation (.forall π) s

Uses 5

Statement usesPath formulas of CTL\(^{\ast}\) · State formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) state formulas

Proof usesSatisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Infinite run

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.