CTL* state-run semantics and canonical labeled executions

4 fully proved

Canonical labeled-execution semantics

DefinitionCTL\(^{\ast}\) state satisfaction over labeled executions#✓fully proved

Satisfaction of a CTL* state formula at a state over canonical Cslib.LTS: E π holds when some infinite labeled execution from the state satisfies π; A π when every infinite labeled execution does.

def UpstreamStateSat (lts : _root_.Cslib.LTS State Label)
    (valuation : State → Atom → Prop) : StateFormula Atom → State → Prop
  | .atom a, s => valuation s a
  | .top, _ => True
  | .not φ, s => ¬ UpstreamStateSat lts valuation φ s
  | .and φ ψ, s => UpstreamStateSat lts valuation φ s ∧
      UpstreamStateSat lts valuation ψ s
  | .exists π, s => ∃ oss μs, oss 0 = s ∧ lts.OmegaExecution oss μs ∧
      UpstreamPathSat lts valuation π oss
  | .forall π, s => ∀ oss μs, oss 0 = s → lts.OmegaExecution oss μs →
      UpstreamPathSat lts valuation π oss

Uses 2 · Used by 2

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

Used byCTL* state-sequence/execution bridge, path formulas · CTL* state-sequence/execution bridge, state formulas

DefinitionCTL\(^{\ast}\) path satisfaction on labeled executions#✓fully proved

Satisfaction of a CTL* path formula on a canonical infinite labeled execution: next drops the first state, while until asks for a target position with the guard before it.

def UpstreamPathSat (lts : _root_.Cslib.LTS State Label)
    (valuation : State → Atom → Prop) : PathFormula Atom → ωSequence State → Prop
  | .state φ, oss => UpstreamStateSat lts valuation φ (oss 0)
  | .not π, oss => ¬ UpstreamPathSat lts valuation π oss
  | .and π ρ, oss => UpstreamPathSat lts valuation π oss ∧
      UpstreamPathSat lts valuation ρ oss
  | .next π, oss => UpstreamPathSat lts valuation π (oss.drop 1)
  | .until π ρ, oss =>
      ∃ k, UpstreamPathSat lts valuation ρ (oss.drop k) ∧
        ∀ j, j < k → UpstreamPathSat lts valuation π (oss.drop j)

Uses 2 · Used by 2

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

Used byCTL* state-sequence/execution bridge, path formulas · CTL* state-sequence/execution bridge, state formulas

The bridge

TheoremCTL* state-sequence/execution bridge, state formulas#✓fully proved

CTL* state-sequence/execution bridge, state formulas. CTL* state satisfaction over lts agrees with satisfaction quantified over canonical OmegaExecutions.

theorem stateSat_iff_upstream (φ : StateFormula Atom) (s : State) :
    StateSat lts valuation φ s ↔
      UpstreamStateSat (lts) valuation φ s

Uses 11

Statement usesState formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) state formulas · CTL\(^{\ast}\) state satisfaction over labeled executions

Proof usesPath formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · CTL\(^{\ast}\) path satisfaction on labeled executions · Infinite run · Infinite state runs lift to labeled executions · Labeled infinite executions give state runs · Shifted function sequences agree with ω-sequence drop · Shifted sequence

TheoremCTL* state-sequence/execution bridge, path formulas#✓fully proved

CTL* state-sequence/execution bridge, path formulas. CTL* path satisfaction on a state run agrees with the canonical labeled-execution presentation on the same state sequence.

theorem pathSat_iff_upstream (π : PathFormula Atom) {run : ℕ → State}
    (hrun : LTS.OmegaRun (lts := lts) run) :
    PathSat lts valuation π run ↔
      UpstreamPathSat (lts) valuation π ⟨run⟩

Uses 11

Statement usesPath formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · CTL\(^{\ast}\) path satisfaction on labeled executions · Infinite run

Proof usesState formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) state formulas · CTL\(^{\ast}\) state satisfaction over labeled executions · Infinite state runs lift to labeled executions · Labeled infinite executions give state runs · Shifted function sequences agree with ω-sequence drop · Shifted sequence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.