Model checking for computation tree logic

19 fully proved

Duality

TheoremEvery state starts a maximal path#✓fully proved

In a labelled transition system, for every state \(s\) there is an infinite run \(s_0, s_1, s_2, \dots\) with \(s_0 = s\), or there are a sequence of states \(s_0, s_1, s_2, \dots\) with \(s_0 = s\) and a \(k\) such that \(s_0, \dots, s_k\) is a finite run of length \(k\) and \(s_k\) is deadlocked, that is, has no outgoing transition.

The proof iterates a chosen successor function and uses the axiom of choice.

theorem exists_maximalPath (s : State) :
    (∃ ss, ss 0 = s ∧ lts.OmegaRun ss) ∨
      (∃ ss k, ss 0 = s ∧ lts.FiniteRun ss k ∧
        ∀ label t, ¬lts.Tr (ss k) label t)

Uses 2 · Used by 1

Statement usesFinite run · Infinite run

Used byOne-step unfolding of universal until, forward direction

TheoremDeadlocked states are exactly those satisfying ¬EX ⊤#✓fully proved

A state \(s\) of a labelled transition system satisfies the CTL formula \(\neg\mathsf{EX}\,\top\), under any valuation of the atoms, if and only if \(s\) is deadlocked: there is no label \(a\) and state \(t\) with a transition from \(s\) to \(t\) labelled \(a\).

theorem not_existsNext_top_iff {s : State} :
    Satisfies lts valuation s (.not (.existsNext .top)) ↔
      ∀ label t, ¬lts.Tr s label t

Uses 2 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas

Used byBad target of the deadlock-correct until duality

TheoremBad target of the deadlock-correct until duality#✓fully proved

Let \(\varphi\) and \(\psi\) be CTL formulas, and write \(t \models \chi\) when the state \(t\) of a labelled transition system satisfies the formula \(\chi\) under a given valuation of the atoms. Then \(t \models \neg\psi \land (\neg\varphi \lor \neg\mathsf{EX}\,\top)\) if and only if \(t \not\models \psi\) and either \(t \not\models \varphi\) or \(t\) is deadlocked, that is, there is no label \(a\) and state \(u\) with a transition from \(t\) to \(u\) labelled \(a\).

theorem forallUntil_bad_iff {φ ψ : Formula Atom} {t : State} :
    Satisfies lts valuation t
        (.and (.not ψ) (Formula.or (.not φ) (.not (.existsNext .top)))) ↔
      ¬Satisfies lts valuation t ψ ∧
        (¬Satisfies lts valuation t φ ∨
          ∀ label u, ¬lts.Tr t label u)

Uses 4 · Used by 2

Statement usesCTL formulas · CTL disjunction · Satisfaction of CTL formulas

Proof usesDeadlocked states are exactly those satisfying ¬EX ⊤

Used byDeadlock-correct duality for universal until · Correctness of the CTL model checker

TheoremOne-step unfolding of universal until, forward direction#✓fully proved

Let \(\varphi\) and \(\psi\) be CTL formulas, and write \(s \models \chi\) when the state \(s\) of a labelled transition system satisfies the formula \(\chi\) under a given valuation of the atoms. If \(s \models \mathsf{A}[\varphi \mathbin{\mathsf{U}} \psi]\), then either \(s \models \psi\), or \(s \models \varphi\), \(s\) has at least one outgoing transition, and every state \(t\) reached from \(s\) by a single transition with any label satisfies \(t \models \mathsf{A}[\varphi \mathbin{\mathsf{U}} \psi]\).

theorem forallUntil_expansion_forward {s : State} {φ ψ : Formula Atom}
    (hAU : Satisfies lts valuation s (.forallUntil φ ψ)) :
    Satisfies lts valuation s ψ ∨
      (Satisfies lts valuation s φ ∧ (∃ label t, lts.Tr s label t) ∧
        ∀ label t, lts.Tr s label t →
          Satisfies lts valuation t (.forallUntil φ ψ))

Uses 6 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas

Proof uses\(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state · Every state starts a maximal path · Finite run · Infinite run

Used byDeadlock-correct duality for universal until

TheoremDeadlock-correct duality for universal until#✓fully proved

Let \(\varphi\) and \(\psi\) be CTL formulas, and write \(s \models \chi\) when the state \(s\) of a labelled transition system satisfies the formula \(\chi\) under a given valuation of the atoms. Then \(s \models \mathsf{A}[\varphi \mathbin{\mathsf{U}} \psi]\) if and only if neither \(s \models \mathsf{E}[\neg\psi \mathbin{\mathsf{U}} (\neg\psi \land (\neg\varphi \lor \neg\mathsf{EX}\,\top))]\) nor \(s \models \mathsf{EG}\,\neg\psi\).

Here \(\neg\mathsf{EX}\,\top\) holds exactly at the deadlocked states, those with no outgoing transition. So \(\mathsf{A}[\varphi \mathbin{\mathsf{U}} \psi]\) fails at \(s\) exactly when some infinite run starting at \(s\) stays in \(\neg\psi\) forever, or some finite run starting at \(s\) stays in \(\neg\psi\) up to a \(\neg\psi\)-state at which \(\varphi\) fails or which is deadlocked.

theorem forallUntil_iff_not {s : State} {φ ψ : Formula Atom} :
    Satisfies lts valuation s (.forallUntil φ ψ) ↔
      ¬(Satisfies lts valuation s
          (.existsUntil (.not ψ)
            (.and (.not ψ)
              (Formula.or (.not φ) (.not (.existsNext .top))))) ∨
        Satisfies lts valuation s (.existsGlobally (.not ψ)))

Uses 7 · Used by 2

Statement usesCTL formulas · CTL disjunction · Satisfaction of CTL formulas

Proof usesBad target of the deadlock-correct until duality · One-step unfolding of universal until, forward direction · Finite run · Infinite run

Used byDeadlock-correct duality for AF · Correctness of the CTL model checker

TheoremCongruence of existential until in its target#✓fully proved

In a labelled transition system with a valuation of atoms, let \(\rho\), \(\alpha\) and \(\beta\) be CTL formulas such that every state satisfies \(\alpha\) if and only if it satisfies \(\beta\). Then every state \(s\) satisfies \(\mathsf{E}[\rho \,\mathsf{U}\, \alpha]\) if and only if it satisfies \(\mathsf{E}[\rho \,\mathsf{U}\, \beta]\).

theorem existsUntil_congr {ρ α β : Formula Atom}
    (h : ∀ t, Satisfies lts valuation t α ↔ Satisfies lts valuation t β)
    {s : State} :
    Satisfies lts valuation s (.existsUntil ρ α) ↔
      Satisfies lts valuation s (.existsUntil ρ β)

Uses 3 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas

Proof usesFinite run

Used byDeadlock-correct duality for AF

TheoremDeadlock-correct duality for AF#✓fully proved

In a labelled transition system with a valuation of atoms, let \(\varphi\) be a CTL formula. A state \(s\) satisfies \(\mathsf{AF}\,\varphi\) if and only if \(s\) satisfies neither \(\mathsf{E}[\neg\varphi \,\mathsf{U}\, (\neg\varphi \wedge \neg\mathsf{EX}\,\top)]\) nor \(\mathsf{EG}\,\neg\varphi\).

This is the case \(\mathsf{A}[\top \,\mathsf{U}\, \varphi]\) of the duality for universal until. The formula \(\neg\mathsf{EX}\,\top\) holds exactly at deadlocked states, so the first disjunct catches finite maximal paths that end at a deadlock without reaching \(\varphi\).

theorem forallFinally_iff_not {s : State} {φ : Formula Atom} :
    Satisfies lts valuation s φ.forallFinally ↔
      ¬(Satisfies lts valuation s
          (.existsUntil (.not φ)
            (.and (.not φ) (.not (.existsNext .top)))) ∨
        Satisfies lts valuation s (.existsGlobally (.not φ)))

Uses 6

Statement usesCTL formulas · The CTL operator AF (inevitably) · Satisfaction of CTL formulas

Proof usesCTL disjunction · Congruence of existential until in its target · Deadlock-correct duality for universal until

TheoremExistential next via the predecessor operator#✓fully proved

In a labelled transition system with a valuation of atoms, let \(\varphi\) be a CTL formula and write \(\mathrm{Sat}(\varphi)\) for the set of states satisfying \(\varphi\). A state \(s\) satisfies \(\mathsf{EX}\,\varphi\) if and only if \(s\) belongs to the existential predecessor set of \(\mathrm{Sat}(\varphi)\), that is, some transition leads from \(s\) to a state satisfying \(\varphi\).

theorem existsNext_iff_preExists {s : State} {φ : Formula Atom} :
    Satisfies lts valuation s (.existsNext φ) ↔
      PreExists lts (fun t => Satisfies lts valuation t φ) s

Uses 3

Statement usesCTL formulas · Existential predecessor operator · Satisfaction of CTL formulas

DefinitionThe existential-until functional#✓fully proved

In a labelled transition system with a valuation of atoms, let \(\varphi\) and \(\psi\) be CTL formulas. The existential-until functional sends a set \(Z\) of states to the set of states \(s\) such that either \(s\) satisfies \(\psi\), or \(s\) satisfies \(\varphi\) and some transition leads from \(s\) to a state in \(Z\).

Its least fixed point is the set of states satisfying \(\mathsf{E}[\varphi \,\mathsf{U}\, \psi]\).

def existsUntilFun (lts : LTS State Label)
    (valuation : State → Atom → Prop) (φ ψ : Formula Atom)
    (Z : State → Prop) : State → Prop :=
  fun s => Satisfies lts valuation s ψ ∨
    (Satisfies lts valuation s φ ∧ PreExists lts Z s)

Uses 3 · Used by 2

Statement usesCTL formulas · Existential predecessor operator · Satisfaction of CTL formulas

Used byThe existential-until functional as a monotone map · Correctness of the finite fixed-point computation of EU

DefinitionThe existential-until functional as a monotone map#✓fully proved

In a labelled transition system with a valuation of atoms, let \(\varphi\) and \(\psi\) be CTL formulas. The map sending a set \(Z\) of states to the set of states \(s\) such that either \(s\) satisfies \(\psi\), or \(s\) satisfies \(\varphi\) and some transition leads from \(s\) to a state in \(Z\), is monotone for inclusion; this is that map, regarded as an order-preserving map on sets of states.

def existsUntilOrderHom (lts : LTS State Label)
    (valuation : State → Atom → Prop) (φ ψ : Formula Atom) :
    (State → Prop) →o (State → Prop) :=
  ⟨existsUntilFun lts valuation φ ψ,
    existsUntilFun_mono lts valuation φ ψ⟩

Uses 4 · Used by 2

Statement usesCTL formulas · Existential predecessor operator · Satisfaction of CTL formulas · The existential-until functional

Used byExistential until as a least fixed point · Correctness of the finite fixed-point computation of EU

TheoremExistential until as a least fixed point#✓fully proved

In a labelled transition system with a valuation of atoms, let \(\varphi\) and \(\psi\) be CTL formulas, write \(\mathrm{Sat}(\chi)\) for the set of states satisfying a formula \(\chi\), and write \(\mathrm{Pre}_\exists(Z)\) for the set of states having a transition into a set \(Z\) of states. Then the set of states satisfying \(\mathsf{E}[\varphi \,\mathsf{U}\, \psi]\) is the least fixed point of the monotone map \(Z \mapsto \mathrm{Sat}(\psi) \cup (\mathrm{Sat}(\varphi) \cap \mathrm{Pre}_\exists(Z))\) on sets of states.

One inclusion is Park induction via the one-step expansion of \(\mathsf{E}[\varphi \,\mathsf{U}\, \psi]\); the other is induction on the length of the witnessing finite run, unfolding the fixed point once per step.

theorem existsUntil_eq_lfp (φ ψ : Formula Atom) :
    (fun s => Satisfies lts valuation s (.existsUntil φ ψ)) =
      (existsUntilOrderHom lts valuation φ ψ).lfp

Uses 7 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas · The existential-until functional as a monotone map

Proof usesExistential predecessor operator · One-step expansion of \(\mathrm{EU}\) · Finite run · Shifted sequence

Used byCorrectness of the finite fixed-point computation of EU

Checker

DefinitionFinite existential predecessor set#✓fully proved

Let a labelled transition system have finitely many states and finitely many labels, with decidable transitions. For a finite set \(Z\) of states, its existential predecessor set is the finite set of states \(s\) for which there are a label \(a\) and a state \(t \in Z\) with a transition from \(s\) to \(t\) labelled \(a\).

It agrees with the existential predecessor operator applied to membership in \(Z\).

def preExistsFin (lts : LTS State Label)
    [∀ s μ t, Decidable (lts.Tr s μ t)] (Z : Finset State) :
    Finset State :=
  Finset.univ.filter (fun s => ∃ μ, ∃ t ∈ Z, lts.Tr s μ t)

Used by 6

Used byFinite existential-globally set · Finite existential-until set · Correctness of the finite fixed-point computation of EG · Correctness of the finite fixed-point computation of EU · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

DefinitionFinite existential-until set#✓fully proved

Let \(\mathcal{T}\) be a labelled transition system with finitely many states and finitely many labels, decidable transitions and decidable equality of states, and let \(A\) and \(B\) be sets of states. For a set \(Z\) of states write \(\mathrm{Pre}_\exists(Z)\) for the set of states having a transition into \(Z\). The existential-until set with side set \(A\) and target set \(B\) is obtained by applying the map \(Z \mapsto B \cup (A \cap \mathrm{Pre}_\exists(Z))\) to the empty set \(n\) times, where \(n\) is the number of states.

Since this map is monotone, the iteration has stabilized after \(n\) steps and the result is its least fixed point.

def eUntilFin (lts : LTS State Label)
    [∀ s μ t, Decidable (lts.Tr s μ t)] (A B : Finset State) :
    Finset State :=
  Finset.lfpFin (fun Z => B ∪ (A ∩ preExistsFin lts Z))

Uses 2 · Used by 3

Statement usesFinite existential predecessor set · Least fixed point of a finset map by finite iteration

Used byCorrectness of the finite fixed-point computation of EU · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

DefinitionFinite existential-globally set#✓fully proved

Let \(\mathcal{T}\) be a labelled transition system with finitely many states and finitely many labels, decidable transitions and decidable equality of states, and let \(A\) be a set of states. For a set \(Z\) of states write \(\mathrm{Pre}_\exists(Z)\) for the set of states having a transition into \(Z\). The existential-globally set of \(A\) is obtained by applying the map \(Z \mapsto A \cap \mathrm{Pre}_\exists(Z)\) to the set of all states \(n\) times, where \(n\) is the number of states.

Since this map is monotone, the iteration has stabilized after \(n\) steps and the result is its greatest fixed point.

def eGloballyFin (lts : LTS State Label)
    [∀ s μ t, Decidable (lts.Tr s μ t)] (A : Finset State) :
    Finset State :=
  Finset.gfpFin (fun Z => A ∩ preExistsFin lts Z)

Uses 2 · Used by 3

Statement usesFinite existential predecessor set · Greatest fixed point of a finset map by finite iteration

Used byCorrectness of the finite fixed-point computation of EG · Correctness of the CTL model checker · Finite-state CTL model checking by structural recursion

TheoremCorrectness of the finite fixed-point computation of EU#✓fully proved

Let a labelled transition system have finitely many states and finitely many labels, with decidable transitions and decidable equality of states, and fix a valuation of the atoms. For a finite set \(Z\) of states let \(\mathrm{Pre}_\exists(Z)\) be the set of states with a transition into \(Z\), and for finite sets \(A\) and \(B\) of states let \(\mathrm{EU}_{\mathrm{fin}}(A, B)\) be the least fixed point of \(Z \mapsto B \cup (A \cap \mathrm{Pre}_\exists(Z))\), computed by finite iteration. Let \(\varphi\) and \(\psi\) be CTL formulas and \(A\) and \(B\) finite sets of states such that a state lies in \(A\) exactly when it satisfies \(\varphi\), and lies in \(B\) exactly when it satisfies \(\psi\). Then every state \(s\) lies in \(\mathrm{EU}_{\mathrm{fin}}(A, B)\) if and only if \(s\) satisfies \(\mathsf{E}[\varphi \mathbin{\mathsf{U}} \psi]\).

theorem mem_eUntilFin_iff {A B : Finset State} {φ ψ : Formula Atom}
    (hA : ∀ t, t ∈ A ↔ Satisfies lts valuation t φ)
    (hB : ∀ t, t ∈ B ↔ Satisfies lts valuation t ψ) (s : State) :
    s ∈ eUntilFin lts A B ↔
      Satisfies lts valuation s (.existsUntil φ ψ)

Uses 10 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas · Finite existential-until set

Proof usesExistential predecessor operator · The existential-until functional · The existential-until functional as a monotone map · Existential until as a least fixed point · Finite existential predecessor set · Least fixed point of a finset map by finite iteration · Finite iteration computes the least fixed point

Used byCorrectness of the CTL model checker

TheoremCorrectness of the finite fixed-point computation of EG#✓fully proved

Let a labelled transition system have finitely many states and finitely many labels, with decidable transitions and decidable equality of states, and fix a valuation of the atoms. For a finite set \(Z\) of states let \(\mathrm{Pre}_\exists(Z)\) be the set of states with a transition into \(Z\), and for a finite set \(A\) of states let \(\mathrm{EG}_{\mathrm{fin}}(A)\) be the greatest fixed point of \(Z \mapsto A \cap \mathrm{Pre}_\exists(Z)\), computed by finite iteration. Let \(\varphi\) be a CTL formula and \(A\) a finite set of states such that a state lies in \(A\) exactly when it satisfies \(\varphi\). Then every state \(s\) lies in \(\mathrm{EG}_{\mathrm{fin}}(A)\) if and only if \(s\) satisfies \(\mathsf{EG}\,\varphi\).

theorem mem_eGloballyFin_iff {A : Finset State} {φ : Formula Atom}
    (hA : ∀ t, t ∈ A ↔ Satisfies lts valuation t φ) (s : State) :
    s ∈ eGloballyFin lts A ↔
      Satisfies lts valuation s (.existsGlobally φ)

Uses 10 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas · Finite existential-globally set

Proof usesExistential predecessor operator · The functional for \(\mathrm{EG}\) · The \(\mathrm{EG}\) functional as a monotone operator · \(\mathsf{EG}\) is a greatest fixed point · Finite existential predecessor set · Greatest fixed point of a finset map by finite iteration · Finite iteration computes the greatest fixed point

Used byCorrectness of the CTL model checker

DefinitionFinite-state CTL model checking by structural recursion#✓fully proved

The set of states satisfying a CTL formula in a finite system, computed by structural recursion: atoms by filtering the valuation, EX by preExistsFin, EU and EG by the finite fixed points eUntilFin and eGloballyFin, and AU by complementing the deadlock-correct duality of Satisfies.forallUntil_iff_not (the bad-target set is built from the complement sets of the subformulas and preExistsFin lts Finset.univ, the set of non-deadlocked states).

Cslib.CTL.sat · 22 lines

def sat (lts : LTS State Label)
    (valuation : State → Atom → Prop)
    [∀ s μ t, Decidable (lts.Tr s μ t)]
    [∀ s a, Decidable (valuation s a)] :
    Formula Atom → Finset State
  | .atom a => Finset.univ.filter (fun s => valuation s a)
  | .top => Finset.univ
  | .not φ => Finset.univ \ sat lts valuation φ
  | .and φ ψ => sat lts valuation φ ∩ sat lts valuation ψ
  | .existsNext φ => preExistsFin lts (sat lts valuation φ)
  | .existsUntil φ ψ =>
      eUntilFin lts (sat lts valuation φ) (sat lts valuation ψ)
  | .existsGlobally φ => eGloballyFin lts (sat lts valuation φ)
  | .forallUntil φ ψ =>
      let satφ := sat lts valuation φ
      let satψ := sat lts valuation ψ
      let notψ := Finset.univ \ satψ
      let badTarget := notψ ∩
        ((Finset.univ \ satφ) ∪
          (Finset.univ \ preExistsFin lts Finset.univ))
      Finset.univ \
        (eUntilFin lts notψ badTarget ∪ eGloballyFin lts notψ)

Uses 4 · Used by 14

Statement usesCTL formulas · Finite existential-globally set · Finite existential-until set · Finite existential predecessor set

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Mutual exclusion under atomic acquisition · Under a butler every philosopher can always still eat · A butler prevents deadlock · Mutual exclusion under a butler · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering · The CTL model checker as a Boolean decision procedure · Correctness of the CTL model checker

TheoremCorrectness of the CTL model checker#✓fully proved

Let a labelled transition system have finitely many states and finitely many labels, with decidable transitions and decidable equality of states, and let the valuation of the atoms be decidable. For every CTL formula \(\varphi\) and every state \(s\), the state \(s\) lies in the set \(\mathrm{sat}(\varphi)\) computed by the model checker if and only if \(s\) satisfies \(\varphi\).

The proof is by induction on \(\varphi\). The temporal cases use the correctness of the finite fixed-point computations of \(\mathsf{EU}\) and \(\mathsf{EG}\), and the \(\mathsf{AU}\) case also identifies the computed bad-target set with the states satisfying the bad-target formula.

theorem mem_sat {φ : Formula Atom} {s : State} :
    s ∈ sat lts valuation φ ↔ Satisfies lts valuation s φ

Uses 12 · Used by 12

Statement usesCTL formulas · Satisfaction of CTL formulas · Finite-state CTL model checking by structural recursion

Proof usesCTL disjunction · Existential predecessor operator · Bad target of the deadlock-correct until duality · Deadlock-correct duality for universal until · Finite existential-globally set · Finite existential-until set · Correctness of the finite fixed-point computation of EG · Correctness of the finite fixed-point computation of EU · Finite existential predecessor set

Used byUnder atomic acquisition every philosopher can always still eat · Atomic acquisition prevents deadlock · Mutual exclusion under atomic acquisition · Under a butler every philosopher can always still eat · A butler prevents deadlock · Mutual exclusion under a butler · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering

DefinitionThe CTL model checker as a Boolean decision procedure#✓fully proved

Let \(\mathcal{T}\) be a labelled transition system with finitely many states and finitely many labels, decidable transitions and decidable equality of states, and let \(V\) be a decidable valuation of atoms at states. For a state \(s\) and a CTL formula \(\varphi\), the model checker returns true exactly when \(s\) belongs to the set of states that the satisfaction-set algorithm computes for \(\varphi\) in \(\mathcal{T}\) under \(V\).

def check (lts : LTS State Label)
    (valuation : State → Atom → Prop)
    [∀ s μ t, Decidable (lts.Tr s μ t)]
    [∀ s a, Decidable (valuation s a)] (s : State)
    (φ : Formula Atom) : Bool :=
  decide (s ∈ sat lts valuation φ)

Uses 2 · Used by 5

Statement usesCTL formulas · Finite-state CTL model checking by structural recursion

Used byAtomic acquisition prevents deadlock · A butler prevents deadlock · The naive protocol can deadlock · A deadlock state of the naive protocol · Resource ordering prevents deadlock for the dining philosophers

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.