Labelled transition systems

TheoremReachability in a labelled transition system is transitive#✓fully proved

In a labelled transition system, say that a state \(s\) can reach a state \(t\) when there is a finite list of labels along which \(s\) makes a multistep transition to \(t\). If \(s\) can reach \(m\) and \(m\) can reach \(t\), then \(s\) can reach \(t\).

The witnessing list of labels is the concatenation of the two given lists.

@[trans]
theorem CanReach.trans {source middle target : State}
    (hsm : lts.CanReach source middle) (hmt : lts.CanReach middle target) :
    lts.CanReach source target

Used by 1

Used by\(\mathsf{EF}\) means reachability

DefinitionShifted sequence#✓fully proved

For a sequence \(s_0, s_1, s_2, \dots\) and a natural number \(k\), the shift of the sequence by \(k\) is the sequence whose \(i\)-th term is \(s_{i+k}\); that is, the suffix starting at index \(k\), re-indexed from \(0\).

def shiftSeq {State : Type*} (ss : ℕ → State) (k : ℕ) : ℕ → State :=
  fun i => ss (i + k)

Used by 17

Used byShifted function sequences agree with ω-sequence drop · One-step expansion of \(\mathsf{EG}\) · One-step expansion of \(\mathrm{EU}\) · The CTL embedding preserves semantics on serial systems · The LTL embedding preserves semantics on every sequence · The LTL embedding preserves semantics at every position · 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 shifted run holds at the shifted state · A run shifted by k starts at its k-th 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 · Existential until as a least fixed point

DefinitionFinite run#✓fully proved

In a labelled transition system, a sequence of states \(s_0, s_1, s_2, \dots\) is a finite run of length \(k\) when for every \(i < k\) there is a label \(a\) such that there is a transition from \(s_i\) to \(s_{i+1}\) labelled \(a\).

The states after index \(k\) are unconstrained.

def FiniteRun (ss : ℕ → State) (k : ℕ) : Prop :=
  ∀ i, i < k → ∃ label, lts.Tr (ss i) label (ss (i + 1))

Used by 15

Used by\(\mathsf{EF}\) via finite runs · \(\mathsf{EF}\) means reachability · Finite runs extend to infinite runs in serial systems · One-step expansion of \(\mathrm{EU}\) · On serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\) · Maximal-path form of \(\mathrm{AF}\) · \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state · Classical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems · Satisfaction of CTL formulas · The CTL embedding preserves semantics on serial systems · Every state starts a maximal path · Congruence of existential until in its target · Existential until as a least fixed point · One-step unfolding of universal until, forward direction · Deadlock-correct duality for universal until

DefinitionInfinite run#✓fully proved

In a labelled transition system, a sequence of states \(s_0, s_1, s_2, \dots\) is an infinite run when for every \(i\) there is a label \(a\) such that there is a transition from \(s_i\) to \(s_{i+1}\) labelled \(a\).

def OmegaRun (ss : ℕ → State) : Prop :=
  ∀ i, ∃ label, lts.Tr (ss i) label (ss (i + 1))

Used by 22

Used byInvariant principle for infinite runs · Infinite state runs lift to labeled executions · Labeled infinite executions give state runs · \(\mathsf{EG}\) is a greatest fixed point · One-step expansion of \(\mathsf{EG}\) · Finite runs extend to infinite runs in serial systems · On serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\) · Maximal-path form of \(\mathrm{AF}\) · \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state · Classical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems · Satisfaction of CTL formulas · The CTL embedding preserves semantics on serial systems · Satisfaction of CTL\(^{\ast}\) path formulas on infinite runs · 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 · No existential path formula holds at a terminal state · Universal path formulas hold vacuously at terminal states · Every state starts a maximal path · One-step unfolding of universal until, forward direction · Deadlock-correct duality for universal until

TheoremInvariant principle for infinite runs#✓fully proved

Let \(P\) be a predicate on the states of a labelled transition system such that, whenever \(P(s)\) holds and there is a transition from \(s\) to \(t\) with some label, \(P(t)\) holds. Then for every infinite run \(s_0, s_1, s_2, \dots\) with \(P(s_0)\), the predicate \(P(s_k)\) holds for every \(k\).

theorem forall_state_of_invariant {run : ℕ → State}
    (hrun : lts.OmegaRun run) {P : State → Prop} (h0 : P (run 0))
    (hstep : ∀ s t, P s → lts.UnlabelledTr s t → P t) :
    ∀ k, P (run k)

Uses 1

Statement usesInfinite run

TheoremInfinite state runs lift to labeled executions#✓fully proved

Select a witnessing label at each step of an infinite state run.

theorem omegaExecution_of_omegaRun {ss : ℕ → State}
    (h : lts.OmegaRun ss) :
    ∃ μs : ωSequence Label, lts.OmegaExecution ⟨ss⟩ μs

Uses 1 · Used by 2

Statement usesInfinite run

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

TheoremLabeled infinite executions give state runs#✓fully proved

Forget the labels of a canonical infinite execution.

theorem omegaRun_of_omegaExecution {oss : ωSequence State}
    {μs : ωSequence Label} (h : lts.OmegaExecution oss μs) :
    lts.OmegaRun (fun i => oss i)

Uses 1 · Used by 2

Statement usesInfinite run

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

TheoremShifted function sequences agree with ω-sequence drop#✓fully proved

Function-sequence suffixes agree with canonical ωSequence.drop.

theorem shiftSeq_eq_drop (ss : ℕ → State) (k : ℕ) :
    (⟨Semantics.shiftSeq ss k⟩ : ωSequence State) =
      ωSequence.drop k ⟨ss⟩

Uses 1 · Used by 2

Statement usesShifted sequence

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

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.