CTL*: state and path formulas

22 fully proved

State and path formulas

InductiveState formulas of CTL\(^{\ast}\)#✓fully proved

State formulas of CTL*: atoms, truth, negation, conjunction, and the path quantifiers E π and A π.

inductive StateFormula (Atom : Type u) where
  | atom (a : Atom) : StateFormula Atom
  | top : StateFormula Atom
  | not (φ : StateFormula Atom) : StateFormula Atom
  | and (φ ψ : StateFormula Atom) : StateFormula Atom
  | exists (π : PathFormula Atom) : StateFormula Atom
  | forall (π : PathFormula Atom) : StateFormula Atom

Used by 18

Used byAlways operator on CTL\(^{\ast}\) path formulas · Embedding of CTL formulas as CTL\(^{\ast}\) state formulas · The CTL embedding preserves semantics on serial systems · Embedding of LTL formulas as CTL\(^{\ast}\) path formulas · Eventually operator on CTL\(^{\ast}\) path formulas · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Always holds on a run iff its argument holds on every suffix · Eventually holds on a run iff its argument holds on some suffix · A state formula on a run holds at its first state · A state formula on a shifted run holds at the shifted state · Satisfaction of CTL\(^{\ast}\) state formulas · \(E\,G\,F\,p\) holds at false in the toggle system · CTL* state-sequence/execution bridge, path formulas · CTL* state-sequence/execution bridge, state formulas · CTL\(^{\ast}\) path satisfaction on labeled executions · CTL\(^{\ast}\) state satisfaction over labeled executions · No existential path formula holds at a terminal state · Universal path formulas hold vacuously at terminal states

InductivePath formulas of CTL\(^{\ast}\)#✓fully proved

Path formulas of CTL*: a state formula at the first position, negation, conjunction, next, and until.

inductive PathFormula (Atom : Type u) where
  | state (φ : StateFormula Atom) : PathFormula Atom
  | not (π : PathFormula Atom) : PathFormula Atom
  | and (π ρ : PathFormula Atom) : PathFormula Atom
  | next (π : PathFormula Atom) : PathFormula Atom
  | until (π ρ : PathFormula Atom) : PathFormula Atom

Used by 19

Used byAlways operator on CTL\(^{\ast}\) path formulas · Embedding of CTL formulas as CTL\(^{\ast}\) state formulas · The CTL embedding preserves semantics on serial systems · Embedding of LTL formulas as CTL\(^{\ast}\) path formulas · Eventually operator on CTL\(^{\ast}\) path formulas · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Always holds on a run iff its argument holds on every suffix · Eventually holds on a run iff its argument holds on some suffix · Next on a run is satisfaction on the shifted run · A state formula on a run holds at its first state · A state formula on a shifted run holds at the shifted state · Satisfaction of CTL\(^{\ast}\) state formulas · \(E\,G\,F\,p\) holds at false in the toggle system · CTL* state-sequence/execution bridge, path formulas · CTL* state-sequence/execution bridge, state formulas · CTL\(^{\ast}\) path satisfaction on labeled executions · CTL\(^{\ast}\) state satisfaction over labeled executions · No existential path formula holds at a terminal state · Universal path formulas hold vacuously at terminal states

Path Formula

DefinitionAlways operator on CTL\(^{\ast}\) path formulas#✓fully proved

G π: π holds at every position, as ¬(⊤ U ¬π).

def alwaysPath (π : PathFormula Atom) : PathFormula Atom :=
  .not (.until (.state .top) (.not π))

Uses 2 · Used by 4

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

Used byEmbedding of CTL formulas as CTL\(^{\ast}\) state formulas · The CTL embedding preserves semantics on serial systems · Always holds on a run iff its argument holds on every suffix · \(E\,G\,F\,p\) holds at false in the toggle system

DefinitionEventually operator on CTL\(^{\ast}\) path formulas#✓fully proved

F π: π holds at some position, as ⊤ U π.

def eventuallyPath (π : PathFormula Atom) : PathFormula Atom :=
  .until (.state .top) π

Uses 2 · Used by 1

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

Used byEventually holds on a run iff its argument holds on some suffix

Satisfaction

DefinitionSatisfaction of CTL\(^{\ast}\) state formulas#✓fully proved

Satisfaction of a CTL* state formula at a state: E π holds when some infinite run from the state satisfies π; A π when every infinite run does.

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

Uses 4 · Used by 8

Statement usesPath formulas of CTL\(^{\ast}\) · State formulas of CTL\(^{\ast}\) · Infinite run · Shifted sequence

Used byThe CTL embedding preserves semantics on serial systems · A state formula on a run holds at its first state · A state formula on a shifted run holds at the shifted state · \(E\,G\,F\,p\) holds at false in the toggle system · CTL* state-sequence/execution bridge, path formulas · CTL* state-sequence/execution bridge, state formulas · No existential path formula holds at a terminal state · Universal path formulas hold vacuously at terminal states

DefinitionSatisfaction of CTL\(^{\ast}\) path formulas on infinite runs#✓fully proved

Satisfaction of a CTL* path formula on an infinite run: next shifts the run, until asks for a target position with the guard before it.

def PathSat (lts : _root_.Cslib.LTS State Label) (valuation : State → Atom → Prop) :
    PathFormula Atom → (ℕ → State) → Prop
  | .state φ, run => StateSat lts valuation φ (run 0)
  | .not π, run => ¬ PathSat lts valuation π run
  | .and π ρ, run => PathSat lts valuation π run ∧ PathSat lts valuation ρ run
  | .next π, run => PathSat lts valuation π (Semantics.shiftSeq run 1)
  | .until π ρ, run =>
      ∃ k, PathSat lts valuation ρ (Semantics.shiftSeq run k) ∧
        ∀ j, j < k → PathSat lts valuation π (Semantics.shiftSeq run j)

Uses 4 · Used by 13

Statement usesPath formulas of CTL\(^{\ast}\) · State formulas of CTL\(^{\ast}\) · Infinite run · Shifted sequence

Used byThe CTL embedding preserves semantics on serial systems · The LTL embedding preserves semantics on every sequence · The LTL embedding preserves semantics at every position · Always holds on a run iff its argument holds on every suffix · Eventually holds on a run iff its argument holds on some suffix · Next on a run is satisfaction on the shifted run · A state formula on a run holds at its first state · A state formula on a shifted run holds at the shifted state · \(E\,G\,F\,p\) holds at false in the toggle system · CTL* state-sequence/execution bridge, path formulas · CTL* state-sequence/execution bridge, state formulas · No existential path formula holds at a terminal state · Universal path formulas hold vacuously at terminal states

TheoremA state formula on a run holds at its first state#✓fully proved

Unfolding: a state formula on a run is satisfaction at its first state.

theorem pathSat_state (φ : StateFormula Atom) (run : ℕ → State) :
    PathSat lts valuation (.state φ) run = StateSat lts valuation φ (run 0)

Uses 4 · Used by 2

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

Used byA state formula on a shifted run holds at the shifted state · \(E\,G\,F\,p\) holds at false in the toggle system

TheoremNext on a run is satisfaction on the shifted run#✓fully proved

Unfolding: next shifts the run.

theorem pathSat_next (π : PathFormula Atom) (run : ℕ → State) :
    PathSat lts valuation (.next π) run =
      PathSat lts valuation π (Semantics.shiftSeq run 1)

Uses 3 · Used by 1

Statement usesPath formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Shifted sequence

Used byThe CTL embedding preserves semantics on serial systems

TheoremA run shifted by k starts at its k-th state#✓fully proved

(shiftSeq run k) 0 = run k: the 0 + k is discharged by Nat.zero_add.

theorem shiftSeq_apply_zero (run : ℕ → State) (k : ℕ) :
    Semantics.shiftSeq run k 0 = run k

Uses 1 · Used by 2

Statement usesShifted sequence

Used byA state formula on a shifted run holds at the shifted state · \(E\,G\,F\,p\) holds at false in the toggle system

TheoremA state formula on a shifted run holds at the shifted state#✓fully proved

A state formula on a shifted run is satisfaction at the shifted position.

theorem pathSat_state_shift (φ : StateFormula Atom) (run : ℕ → State) (k : ℕ) :
    PathSat lts valuation (.state φ) (Semantics.shiftSeq run k) =
      StateSat lts valuation φ (run k)

Uses 7 · Used by 1

Statement usesPath formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · State formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) state formulas · Shifted sequence

Proof usesA state formula on a run holds at its first state · A run shifted by k starts at its k-th state

Used byThe CTL embedding preserves semantics on serial systems

TheoremAlways holds on a run iff its argument holds on every suffix#✓fully proved

G π holds on a run iff π holds on every suffix.

theorem pathSat_always (run : ℕ → State) :
    PathSat lts valuation (π.alwaysPath) run ↔
      ∀ i, PathSat lts valuation π (Semantics.shiftSeq run i)

Uses 5 · Used by 2

Statement usesPath formulas of CTL\(^{\ast}\) · Always operator on CTL\(^{\ast}\) path formulas · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Shifted sequence

Proof usesState formulas of CTL\(^{\ast}\)

Used byThe CTL embedding preserves semantics on serial systems · \(E\,G\,F\,p\) holds at false in the toggle system

TheoremEventually holds on a run iff its argument holds on some suffix#✓fully proved

F π holds on a run iff π holds on some suffix.

theorem pathSat_eventually (run : ℕ → State) :
    PathSat lts valuation (π.eventuallyPath) run ↔
      ∃ k, PathSat lts valuation π (Semantics.shiftSeq run k)

Uses 5

Statement usesPath formulas of CTL\(^{\ast}\) · Eventually operator on CTL\(^{\ast}\) path formulas · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Shifted sequence

Proof usesState formulas of CTL\(^{\ast}\)

DefinitionEmbedding of LTL formulas as CTL\(^{\ast}\) path formulas#✓fully proved

The LTL embedding: every LTL formula is a CTL* path formula.

def embedLTL : LTL.Formula Atom → PathFormula Atom
  | .atom a => .state (.atom a)
  | .top => .state .top
  | .not φ => .not (embedLTL φ)
  | .and φ ψ => .and (embedLTL φ) (embedLTL ψ)
  | .next φ => .next (embedLTL φ)
  | .until φ ψ => .until (embedLTL φ) (embedLTL ψ)

Uses 3 · Used by 2

Statement usesPath formulas of CTL\(^{\ast}\) · State formulas of CTL\(^{\ast}\) · Formulas of linear temporal logic

Used byThe LTL embedding preserves semantics on every sequence · The LTL embedding preserves semantics at every position

TheoremThe LTL embedding preserves semantics on every sequence#✓fully proved

The LTL embedding preserves semantics on every state sequence, including sequences that are not valid runs of lts.

theorem embedLTL_sat (φ : LTL.Formula Atom) :
    ∀ run, PathSat lts valuation (embedLTL φ) run ↔
      LTL.Word.Satisfies valuation ⟨run⟩ φ

Uses 5 · Used by 1

Statement usesSatisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Embedding of LTL formulas as CTL\(^{\ast}\) path formulas · Formulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

Proof usesShifted sequence

Used byThe LTL embedding preserves semantics at every position

TheoremThe LTL embedding preserves semantics at every position#✓fully proved

The structural LTL embedding also agrees at every position, without assuming the sequence is a valid transition run.

theorem embedLTL_sat_at (φ : LTL.Formula Atom) (run : ℕ → State)
    (k : ℕ) :
    PathSat lts valuation (embedLTL φ) (Semantics.shiftSeq run k) ↔
      LTL.Word.SatisfiesAt valuation ⟨run⟩ k φ

Uses 6

Statement usesSatisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Embedding of LTL formulas as CTL\(^{\ast}\) path formulas · Formulas of linear temporal logic · Satisfaction at a position · Shifted sequence

Proof usesThe LTL embedding preserves semantics on every sequence

DefinitionEmbedding of CTL formulas as CTL\(^{\ast}\) state formulas#✓fully proved

The CTL embedding: every CTL formula is a CTL* state formula. EG φ is E G (state φ); AU is A (state φ U state ψ).

def embedCTL : CTL.Formula Atom → StateFormula Atom
  | .atom a => .atom a
  | .top => .top
  | .not φ => .not (embedCTL φ)
  | .and φ ψ => .and (embedCTL φ) (embedCTL ψ)
  | .existsNext φ => .exists (.next (.state (embedCTL φ)))
  | .existsUntil φ ψ => .exists (.until (.state (embedCTL φ)) (.state (embedCTL ψ)))
  | .existsGlobally φ => .exists (.alwaysPath (.state (embedCTL φ)))
  | .forallUntil φ ψ => .forall (.until (.state (embedCTL φ)) (.state (embedCTL ψ)))

Uses 4 · Used by 1

Statement usesCTL formulas · Path formulas of CTL\(^{\ast}\) · Always operator on CTL\(^{\ast}\) path formulas · State formulas of CTL\(^{\ast}\)

Used byThe CTL embedding preserves semantics on serial systems

TheoremThe CTL embedding preserves semantics on serial systems#✓fully proved

The CTL embedding preserves semantics on serial systems.

theorem embedCTL_sat (hser : CTL.Serial lts) (φ : CTL.Formula Atom) :
    ∀ {s : State}, StateSat lts valuation (embedCTL φ) s ↔
      CTL.Satisfies lts valuation s φ

Uses 16

Statement usesCTL formulas · Satisfaction of CTL formulas · Serial transition systems · Satisfaction of CTL\(^{\ast}\) state formulas · Embedding of CTL formulas as CTL\(^{\ast}\) state formulas

Proof usesFinite runs extend to infinite runs in serial systems · Path formulas of CTL\(^{\ast}\) · Always operator on CTL\(^{\ast}\) path formulas · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · State formulas of CTL\(^{\ast}\) · Always holds on a run iff its argument holds on every suffix · Next on a run is satisfaction on the shifted run · A state formula on a shifted run holds at the shifted state · Finite run · Infinite run · Shifted sequence

DefinitionToggle transition system#✓fully proved

The toggle system: every transition flips the state.

def toggleLTS : _root_.Cslib.LTS Bool Unit where
  Tr := fun s _ t => t = !s

Used by 2

Used by\(E\,G\,F\,p\) holds at false in the toggle system · The toggle system is serial

DefinitionValuation of the toggle system#✓fully proved

The valuation: p holds exactly at true.

def toggleValuation : Bool → Unit → Prop := fun s _ => s = true

Used by 1

Used by\(E\,G\,F\,p\) holds at false in the toggle system

TheoremThe toggle system is serial#✓fully proved

The toggle system is serial: every state has a successor.

theorem toggle_serial : CTL.Serial toggleLTS

Uses 2

Statement usesSerial transition systems · Toggle transition system

DefinitionAlternating run of the toggle system#✓fully proved

The alternating run of the toggle system: false, true, false, true, ..., defined by recursion so each step flips the state.

def toggleRun : ℕ → Bool
  | 0 => false
  | n + 1 => !toggleRun n

Used by 1

Used by\(E\,G\,F\,p\) holds at false in the toggle system

Theorem\(E\,G\,F\,p\) holds at false in the toggle system#✓fully proved

E G F p holds at false in the toggle system: the alternating run visits true at every other position. This example makes no claim of an expressiveness separation.

theorem toggle_egf_p :
    StateSat toggleLTS toggleValuation
      (.exists (.alwaysPath (.until (.state .top) (.state (.atom ())))))
      false

Uses 13

Statement usesPath formulas of CTL\(^{\ast}\) · Always operator on CTL\(^{\ast}\) path formulas · State formulas of CTL\(^{\ast}\) · Satisfaction of CTL\(^{\ast}\) state formulas · Toggle transition system · Valuation of the toggle system

Proof usesSatisfaction of CTL\(^{\ast}\) path formulas on infinite runs · Always holds on a run iff its argument holds on every suffix · A state formula on a run holds at its first state · A run shifted by k starts at its k-th state · Alternating run of the toggle system · Infinite run · Shifted sequence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.