Computation tree logic

31 fully proved

CTL

InductiveCTL formulas#✓fully proved

The formulas of computation tree logic over a type \(A\) of atoms are generated as follows: every atom \(a \in A\) is a formula, \(\top\) is a formula, and if \(\varphi\) and \(\psi\) are formulas then so are the negation \(\neg\varphi\), the conjunction \(\varphi \land \psi\), the existential next \(\mathsf{EX}\,\varphi\), the existential until \(\mathsf{E}[\varphi\,\mathsf{U}\,\psi]\), the existential globally \(\mathsf{EG}\,\varphi\) and the universal until \(\mathsf{A}[\varphi\,\mathsf{U}\,\psi]\).

The universal until is primitive rather than the classical translation through \(\mathsf{EU}\) and \(\mathsf{EG}\), which is unsound on transition systems with deadlocked states.

inductive Formula (Atom : Type u) : Type u where
  | atom (a : Atom) : Formula Atom
  | top : Formula Atom
  | not (φ : Formula Atom) : Formula Atom
  | and (φ ψ : Formula Atom) : Formula Atom
  | existsNext (φ : Formula Atom) : Formula Atom
  | existsUntil (φ ψ : Formula Atom) : Formula Atom
  | existsGlobally (φ : Formula Atom) : Formula Atom
  | forallUntil (φ ψ : Formula Atom) : Formula Atom

Used by 58

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 deadlock formula · The naive protocol can deadlock · A deadlock state of the naive protocol · Mutual exclusion under the naive protocol · Neighbours-apart formula · Every philosopher can still eat under resource ordering · Resource ordering prevents deadlock for the dining philosophers · Neighbours never eat together under resource ordering · Falsity in CTL · Exists finally · \(\mathsf{EF}\) is a least fixed point · One-step expansion of \(\mathsf{EF}\) · The \(\mathsf{EF}\) functional · \(\mathsf{EF}\) via finite runs · \(\mathsf{EF}\) means reachability · The \(\mathsf{EF}\) operator · \(\mathsf{EG}\) is a greatest fixed point · One-step expansion of \(\mathsf{EG}\) · The functional for \(\mathrm{EG}\) · The \(\mathrm{EG}\) functional as a monotone operator · One-step expansion of \(\mathrm{EU}\) · The CTL operator AF (inevitably) · \(\mathrm{AF}\) at a deadlocked state · On serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\) · Maximal-path form of \(\mathrm{AF}\) · The CTL operator \(\mathrm{AG}\) · \(\mathrm{AG}\) holds iff every reachable state satisfies the formula · The CTL operator \(\mathsf{AX}\) · Characterization of \(\mathsf{AX}\) · \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state · Classical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems · CTL bi-implication · CTL implication · CTL disjunction · Satisfaction of CTL formulas · Embedding of CTL formulas as CTL\(^{\ast}\) state formulas · The CTL embedding preserves semantics on serial systems · The CTL model checker as a Boolean decision procedure · Existential next via the predecessor operator · Congruence of existential until in its target · Existential until as a least fixed point · The existential-until functional · The existential-until functional as a monotone map · Deadlock-correct duality for AF · Bad target of the deadlock-correct until duality · One-step unfolding of universal until, forward direction · Deadlock-correct duality for universal until · Correctness of the finite fixed-point computation of EG · Correctness of the finite fixed-point computation of EU · Correctness of the CTL model checker · Deadlocked states are exactly those satisfying ¬EX ⊤ · Finite-state CTL model checking by structural recursion

Formula

DefinitionFalsity in CTL#✓fully proved

The CTL formula \(\bot\) (falsity) is the negation \(\neg\top\) of the formula \(\top\) (truth).

def bot : Formula Atom := .not .top

Uses 1

Statement usesCTL formulas

DefinitionCTL disjunction#✓fully proved

For CTL formulas \(\varphi\) and \(\psi\), the disjunction \(\varphi \lor \psi\) is defined as \(\neg(\neg\varphi \land \neg\psi)\).

def or (φ ψ : Formula Atom) : Formula Atom :=
  .not (.and (.not φ) (.not ψ))

Uses 1 · Used by 5

Statement usesCTL formulas

Used byCTL implication · Deadlock-correct duality for AF · Bad target of the deadlock-correct until duality · Deadlock-correct duality for universal until · Correctness of the CTL model checker

DefinitionCTL implication#✓fully proved

For CTL formulas \(\varphi\) and \(\psi\), the implication \(\varphi \to \psi\) is defined as the disjunction \(\neg\varphi \lor \psi\).

def imp (φ ψ : Formula Atom) : Formula Atom := or (.not φ) ψ

Uses 2 · Used by 1

Statement usesCTL formulas · CTL disjunction

Used byCTL bi-implication

DefinitionCTL bi-implication#✓fully proved

For CTL formulas \(\varphi\) and \(\psi\), the bi-implication \(\varphi \leftrightarrow \psi\) is defined as the conjunction \((\varphi \to \psi) \land (\psi \to \varphi)\) of the two implications.

def iff (φ ψ : Formula Atom) : Formula Atom :=
  .and (imp φ ψ) (imp ψ φ)

Uses 2

Statement usesCTL formulas · CTL implication

DefinitionExists finally#✓fully proved

For a CTL formula \(\varphi\), the formula \(\mathsf{EF}\,\varphi\) is the existential until \(\mathsf{E}[\top \mathbin{\mathsf{U}} \varphi]\) with \(\top\) on the left.

A state satisfies \(\mathsf{EF}\,\varphi\) exactly when some state reachable from it satisfies \(\varphi\).

def existsFinally (φ : Formula Atom) : Formula Atom :=
  .existsUntil .top φ

Uses 1 · Used by 10

Statement usesCTL formulas

Used byUnder atomic acquisition every philosopher can always still eat · Under a butler every philosopher can always still eat · The naive protocol can deadlock · Every philosopher can still eat under resource ordering · \(\mathsf{EF}\) is a least fixed point · One-step expansion of \(\mathsf{EF}\) · \(\mathsf{EF}\) via finite runs · \(\mathsf{EF}\) means reachability · The CTL operator \(\mathrm{AG}\) · \(\mathrm{AG}\) holds iff every reachable state satisfies the formula

DefinitionThe CTL operator \(\mathsf{AX}\)#✓fully proved

For a CTL formula \(\varphi\), the formula \(\mathsf{AX}\,\varphi\) ("on all next states, \(\varphi\)") is defined as \(\neg\,\mathsf{EX}\,\neg\varphi\).

It holds at a state exactly when every successor of that state satisfies \(\varphi\), so it holds vacuously at a deadlocked state.

def forallNext (φ : Formula Atom) : Formula Atom :=
  .not (.existsNext (.not φ))

Uses 1 · Used by 1

Statement usesCTL formulas

Used byCharacterization of \(\mathsf{AX}\)

DefinitionThe CTL operator AF (inevitably)#✓fully proved

AF φ: every maximal path reaches a state satisfying φ, as A[⊤ U φ].

def forallFinally (φ : Formula Atom) : Formula Atom :=
  .forallUntil .top φ

Uses 1 · Used by 4

Statement usesCTL formulas

Used by\(\mathrm{AF}\) at a deadlocked state · On serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\) · Maximal-path form of \(\mathrm{AF}\) · Deadlock-correct duality for AF

DefinitionThe CTL operator \(\mathrm{AG}\)#✓fully proved

For a CTL formula \(\varphi\), the formula \(\mathrm{AG}\,\varphi\) is \(\neg\,\mathrm{EF}\,\neg\varphi\). It holds at a state exactly when every state reachable from it satisfies \(\varphi\).

def forallGlobally (φ : Formula Atom) : Formula Atom :=
  .not (existsFinally (.not φ))

Uses 2 · Used by 11

Statement usesCTL formulas · Exists finally

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 · 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 · \(\mathrm{AG}\) holds iff every reachable state satisfies the formula

CTL

DefinitionSatisfaction of CTL formulas#✓fully proved

Fix a labelled transition system and a valuation saying which atoms hold at which states. Satisfaction of a CTL formula at a state \(s\) is defined by recursion on the formula. An atom \(a\) holds at \(s\) when the valuation makes \(a\) true at \(s\); \(\top\) always holds; \(\neg\varphi\) holds when \(\varphi\) does not; \(\varphi \land \psi\) holds when both \(\varphi\) and \(\psi\) hold; \(\mathsf{EX}\,\varphi\) holds when there is a transition from \(s\), under some label, to a state satisfying \(\varphi\); \(\mathsf{E}[\varphi\,\mathsf{U}\,\psi]\) holds when some finite run \(s = s_0, s_1, \dots, s_k\) has \(\psi\) at \(s_k\) and \(\varphi\) at every \(s_j\) with \(j < k\); \(\mathsf{EG}\,\varphi\) holds when some infinite run \(s = s_0, s_1, \dots\) has \(\varphi\) at every state; and \(\mathsf{A}[\varphi\,\mathsf{U}\,\psi]\) holds when, first, every infinite run \(s = s_0, s_1, \dots\) has some \(k\) with \(\psi\) at \(s_k\) and \(\varphi\) at every \(s_j\) with \(j < k\), and second, every finite run \(s = s_0, s_1, \dots, s_k\) whose last state \(s_k\) has no outgoing transition under any label has some \(j \le k\) with \(\psi\) at \(s_j\) and \(\varphi\) at every \(s_i\) with \(i < j\).

Cslib.CTL.Satisfies · 26 lines

def Satisfies (lts : LTS State Label)
    (valuation : State → Atom → Prop) (state : State) :
    Formula Atom → Prop
  | .atom a => valuation state a
  | .top => True
  | .not φ => ¬Satisfies lts valuation state φ
  | .and φ ψ =>
      Satisfies lts valuation state φ ∧ Satisfies lts valuation state ψ
  | .existsNext φ =>
      ∃ label next, lts.Tr state label next ∧
        Satisfies lts valuation next φ
  | .existsUntil φ ψ =>
      ∃ ss k, ss 0 = state ∧ lts.FiniteRun ss k ∧
        Satisfies lts valuation (ss k) ψ ∧
          ∀ j, j < k → Satisfies lts valuation (ss j) φ
  | .existsGlobally φ =>
      ∃ ss, ss 0 = state ∧ lts.OmegaRun ss ∧
        ∀ i, Satisfies lts valuation (ss i) φ
  | .forallUntil φ ψ =>
      (∀ ss, ss 0 = state → lts.OmegaRun ss →
        ∃ k, Satisfies lts valuation (ss k) ψ ∧
          ∀ j, j < k → Satisfies lts valuation (ss j) φ) ∧
      (∀ ss k, ss 0 = state → lts.FiniteRun ss k →
        (∀ label t, ¬lts.Tr (ss k) label t) →
        ∃ j, j ≤ k ∧ Satisfies lts valuation (ss j) ψ ∧
          ∀ i, i < j → Satisfies lts valuation (ss i) φ)

Uses 3 · Used by 44

Statement usesCTL formulas · Finite run · Infinite run

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 · \(\mathsf{EF}\) is a least fixed point · One-step expansion of \(\mathsf{EF}\) · The \(\mathsf{EF}\) functional · \(\mathsf{EF}\) via finite runs · \(\mathsf{EF}\) means reachability · The \(\mathsf{EF}\) operator · \(\mathsf{EG}\) is a greatest fixed point · One-step expansion of \(\mathsf{EG}\) · The functional for \(\mathrm{EG}\) · The \(\mathrm{EG}\) functional as a monotone operator · One-step expansion of \(\mathrm{EU}\) · \(\mathrm{AF}\) at a deadlocked state · On serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\) · Maximal-path form of \(\mathrm{AF}\) · \(\mathrm{AG}\) holds iff every reachable state satisfies the formula · Characterization of \(\mathsf{AX}\) · \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state · Classical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems · The CTL embedding preserves semantics on serial systems · Existential next via the predecessor operator · Congruence of existential until in its target · Existential until as a least fixed point · The existential-until functional · The existential-until functional as a monotone map · Deadlock-correct duality for AF · Bad target of the deadlock-correct until duality · One-step unfolding of universal until, forward direction · Deadlock-correct duality for universal until · Correctness of the finite fixed-point computation of EG · Correctness of the finite fixed-point computation of EU · Correctness of the CTL model checker · Deadlocked states are exactly those satisfying ¬EX ⊤

DefinitionExistential predecessor operator#✓fully proved

For a labelled transition system and a predicate \(Z\) on its states, a state \(s\) satisfies \(\mathrm{Pre}_\exists(Z)\) when some successor of \(s\) satisfies \(Z\): there are a label \(a\) and a state \(t\) satisfying \(Z\) with a transition from \(s\) to \(t\) labelled \(a\).

def PreExists (lts : LTS State Label) (Z : State → Prop)
    (s : State) : Prop :=
  ∃ label t, lts.Tr s label t ∧ Z t

Used by 12

Used by\(\mathsf{EF}\) is a least fixed point · The \(\mathsf{EF}\) functional · The \(\mathsf{EF}\) operator · The functional for \(\mathrm{EG}\) · The \(\mathrm{EG}\) functional as a monotone operator · Existential next via the predecessor operator · Existential until as a least fixed point · The existential-until functional · The existential-until functional as a monotone map · Correctness of the finite fixed-point computation of EG · Correctness of the finite fixed-point computation of EU · Correctness of the CTL model checker

DefinitionSerial transition systems#✓fully proved

A labelled transition system is serial (total) when every state \(s\) has a successor: there are a label \(a\) and a state \(t\) with a transition from \(s\) to \(t\) labelled \(a\).

A serial system has no deadlocked states, and every maximal path in it is infinite.

def Serial (lts : LTS State Label) : Prop :=
  ∀ s, ∃ label t, lts.Tr s label t

Used by 5

Used byFinite runs extend to infinite runs in serial systems · On serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\) · Classical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems · The CTL embedding preserves semantics on serial systems · The toggle system is serial

TheoremFinite runs extend to infinite runs in serial systems#✓fully proved

In a serial labelled transition system, if \(s_0, s_1, s_2, \dots\) is a finite run of length \(k\), then there is an infinite run \(s'_0, s'_1, s'_2, \dots\) with \(s'_i = s_i\) for every \(i \le k\).

The extension iterates a chosen successor function from \(s_k\), so it uses the axiom of choice.

theorem exists_omegaRun_extending_of_serial (hser : Serial lts)
    {ss : ℕ → State} {k : ℕ} (hrun : lts.FiniteRun ss k) :
    ∃ ss', (∀ i, i ≤ k → ss' i = ss i) ∧ lts.OmegaRun ss'

Uses 3 · Used by 2

Statement usesSerial transition systems · Finite run · Infinite run

Used byClassical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems · The CTL embedding preserves semantics on serial systems

Satisfaction

Theorem\(\mathsf{EF}\) via finite runs#✓fully proved

Let \(\varphi\) be a CTL formula. In a labelled transition system with a valuation of the atoms at its states, a state \(s\) satisfies \(\mathsf{EF}\,\varphi\) if and only if there are a sequence of states \(s_0, s_1, s_2, \dots\) with \(s_0 = s\) and a natural number \(k\) such that the sequence is a finite run of length \(k\) and \(s_k\) satisfies \(\varphi\).

theorem existsFinally_iff :
    Satisfies lts valuation s φ.existsFinally ↔
      ∃ ss k, ss 0 = s ∧ lts.FiniteRun ss k ∧
        Satisfies lts valuation (ss k) φ

Uses 4 · Used by 1

Statement usesCTL formulas · Exists finally · Satisfaction of CTL formulas · Finite run

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

TheoremOne-step expansion of \(\mathrm{EU}\)#✓fully proved

Let \(\varphi\) and \(\psi\) be CTL formulas and \(s\) a state of a labelled transition system with a valuation of the atoms. Then \(s\) satisfies \(\mathrm{E}[\varphi \mathbin{\mathrm{U}} \psi]\) if and only if either \(s\) satisfies \(\psi\), or \(s\) satisfies \(\varphi\) and some successor of \(s\) satisfies \(\mathrm{E}[\varphi \mathbin{\mathrm{U}} \psi]\).

theorem existsUntil_expansion :
    Satisfies lts valuation s (.existsUntil φ ψ) ↔
      Satisfies lts valuation s ψ ∨
        (Satisfies lts valuation s φ ∧
          Satisfies lts valuation s (.existsNext (.existsUntil φ ψ)))

Uses 4 · Used by 2

Statement usesCTL formulas · Satisfaction of CTL formulas

Proof usesFinite run · Shifted sequence

Used byOne-step expansion of \(\mathsf{EF}\) · Existential until as a least fixed point

Theorem\(\mathsf{EF}\) means reachability#✓fully proved

Let \(\varphi\) be a CTL formula. In a labelled transition system with a valuation of the atoms at its states, a state \(s\) satisfies \(\mathsf{EF}\,\varphi\) if and only if some state \(t\) reachable from \(s\) by a finite, possibly empty, sequence of transitions satisfies \(\varphi\).

theorem existsFinally_iff_reachable :
    Satisfies lts valuation s φ.existsFinally ↔
      ∃ t, lts.CanReach s t ∧ Satisfies lts valuation t φ

Uses 6 · Used by 2

Statement usesCTL formulas · Exists finally · Satisfaction of CTL formulas

Proof uses\(\mathsf{EF}\) via finite runs · Reachability in a labelled transition system is transitive · Finite run

Used by\(\mathsf{EF}\) is a least fixed point · \(\mathrm{AG}\) holds iff every reachable state satisfies the formula

Theorem\(\mathrm{AG}\) holds iff every reachable state satisfies the formula#✓fully proved

Let \(\varphi\) be a CTL formula and \(s\) a state of a labelled transition system with a valuation of the atoms. Then \(s\) satisfies \(\mathrm{AG}\,\varphi\) if and only if every state \(t\) reachable from \(s\) (through a finite sequence of transitions, possibly empty) satisfies \(\varphi\).

theorem forallGlobally_iff_reachable :
    Satisfies lts valuation s φ.forallGlobally ↔
      ∀ t, lts.CanReach s t → Satisfies lts valuation t φ

Uses 5

Statement usesCTL formulas · The CTL operator \(\mathrm{AG}\) · Satisfaction of CTL formulas

Proof usesExists finally · \(\mathsf{EF}\) means reachability

TheoremCharacterization of \(\mathsf{AX}\)#✓fully proved

Let \(s\) be a state of a labelled transition system with an atom valuation, and let \(\varphi\) be a CTL formula. Then \(s\) satisfies \(\mathsf{AX}\,\varphi\) if and only if every state \(t\) with a transition from \(s\) to \(t\), under any label, satisfies \(\varphi\).

theorem forallNext_iff :
    Satisfies lts valuation s φ.forallNext ↔
      ∀ label t, lts.Tr s label t → Satisfies lts valuation t φ

Uses 3

Statement usesCTL formulas · The CTL operator \(\mathsf{AX}\) · Satisfaction of CTL formulas

TheoremMaximal-path form of \(\mathrm{AF}\)#✓fully proved

Let \(\varphi\) be a CTL formula and \(s\) a state of a labelled transition system with a valuation of the atoms. Then \(s\) satisfies \(\mathrm{AF}\,\varphi\) if and only if both of the following hold: for every infinite run \(s_0, s_1, s_2, \dots\) with \(s_0 = s\) there is some \(k\) such that \(s_k\) satisfies \(\varphi\); and for every finite run \(s_0, s_1, s_2, \dots\) of length \(k\) with \(s_0 = s\) whose endpoint \(s_k\) has no outgoing transition, there is some \(j \le k\) such that \(s_j\) satisfies \(\varphi\).

theorem forallFinally_iff_omega_and_finite :
    Satisfies lts valuation s φ.forallFinally ↔
      (∀ ss, ss 0 = s → lts.OmegaRun ss →
        ∃ k, Satisfies lts valuation (ss k) φ) ∧
      (∀ ss k, ss 0 = s → lts.FiniteRun ss k →
        (∀ label t, ¬lts.Tr (ss k) label t) →
        ∃ j, j ≤ k ∧ Satisfies lts valuation (ss j) φ)

Uses 5 · Used by 1

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

Used byOn serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\)

Theorem\(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state#✓fully proved

Let \(s\) be a state of a labelled transition system with an atom valuation, and suppose that \(s\) is deadlocked: there is no transition from \(s\) under any label. Then for all CTL formulas \(\varphi\) and \(\psi\), \(s\) satisfies \(\mathsf{A}[\varphi\,\mathsf{U}\,\psi]\) if and only if \(s\) satisfies \(\psi\).

The infinite-run condition is vacuous, since an infinite run needs a step at index \(0\), and the constant finite run of length \(0\) forces \(\psi\) at \(s\) itself.

theorem forallUntil_deadlock
    (hdead : ∀ label t, ¬lts.Tr s label t) :
    Satisfies lts valuation s (.forallUntil φ ψ) ↔
      Satisfies lts valuation s ψ

Uses 4 · Used by 2

Statement usesCTL formulas · Satisfaction of CTL formulas

Proof usesFinite run · Infinite run

Used by\(\mathrm{AF}\) at a deadlocked state · One-step unfolding of universal until, forward direction

Theorem\(\mathrm{AF}\) at a deadlocked state#✓fully proved

Let \(\varphi\) be a CTL formula and \(s\) a state of a labelled transition system with a valuation of the atoms. If \(s\) has no outgoing transition, then \(s\) satisfies \(\mathrm{AF}\,\varphi\) if and only if \(s\) satisfies \(\varphi\).

theorem forallFinally_deadlock
    (hdead : ∀ label t, ¬lts.Tr s label t) :
    Satisfies lts valuation s φ.forallFinally ↔
      Satisfies lts valuation s φ

Uses 4

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

Proof uses\(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) at a deadlocked state

TheoremOn serial systems \(\mathrm{AF}\) is \(\neg\mathrm{EG}\,\neg\)#✓fully proved

Let \(\varphi\) be a CTL formula and \(s\) a state of a serial labelled transition system with a valuation of the atoms. Then \(s\) satisfies \(\mathrm{AF}\,\varphi\) if and only if \(s\) does not satisfy \(\mathrm{EG}\,\neg\varphi\).

A serial system has no deadlocked states, so every maximal path is infinite and \(\mathrm{AF}\) recovers its classical form.

theorem forallFinally_iff_not_existsGlobally_not_of_serial
    (hser : Serial lts) :
    Satisfies lts valuation s φ.forallFinally ↔
      ¬Satisfies lts valuation s (.existsGlobally (.not φ))

Uses 7

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

Proof usesMaximal-path form of \(\mathrm{AF}\) · Finite run · Infinite run

TheoremClassical form of \(\mathsf{A}(\varphi\,\mathsf{U}\,\psi)\) on serial systems#✓fully proved

Let \(s\) be a state of a serial labelled transition system with an atom valuation, and let \(\varphi\) and \(\psi\) be CTL formulas. Then \(s\) satisfies \(\mathsf{A}[\varphi\,\mathsf{U}\,\psi]\) if and only if \(s\) satisfies neither \(\mathsf{E}[\neg\psi\,\mathsf{U}\,(\neg\varphi \land \neg\psi)]\) nor \(\mathsf{EG}\,\neg\psi\). That is, no finite run from \(s\) ends at a state satisfying \(\neg\varphi \land \neg\psi\) with \(\neg\psi\) at all earlier states, and no infinite run from \(s\) has \(\neg\psi\) at every state.

The forward direction extends an \(\mathsf{EU}\) witness to an infinite run; the backward direction takes, on each infinite run, the least \(\psi\)-position and derives an \(\mathsf{EU}\) witness from any earlier \(\neg\varphi\)-position.

theorem forallUntil_iff_classical_of_serial (hser : Serial lts) :
    Satisfies lts valuation s (.forallUntil φ ψ) ↔
      ¬(Satisfies lts valuation s
          (.existsUntil (.not ψ) (.and (.not φ) (.not ψ))) ∨
        Satisfies lts valuation s (.existsGlobally (.not ψ)))

Uses 6

Statement usesCTL formulas · Satisfaction of CTL formulas · Serial transition systems

Proof usesFinite runs extend to infinite runs in serial systems · Finite run · Infinite run

TheoremOne-step expansion of \(\mathsf{EF}\)#✓fully proved

Let \(\varphi\) be a CTL formula. In a labelled transition system with a valuation of the atoms at its states, a state \(s\) satisfies \(\mathsf{EF}\,\varphi\) if and only if \(s\) satisfies \(\varphi\) or \(s\) satisfies \(\mathsf{EX}\,\mathsf{EF}\,\varphi\), that is, some successor of \(s\) satisfies \(\mathsf{EF}\,\varphi\).

theorem existsFinally_expansion :
    Satisfies lts valuation s φ.existsFinally ↔
      Satisfies lts valuation s φ ∨
        Satisfies lts valuation s (.existsNext φ.existsFinally)

Uses 4 · Used by 1

Statement usesCTL formulas · Exists finally · Satisfaction of CTL formulas

Proof usesOne-step expansion of \(\mathrm{EU}\)

Used by\(\mathsf{EF}\) is a least fixed point

TheoremOne-step expansion of \(\mathsf{EG}\)#✓fully proved

Let \(\varphi\) be a CTL formula. In a labelled transition system with a valuation of the atoms at its states, a state \(s\) satisfies \(\mathsf{EG}\,\varphi\) if and only if \(s\) satisfies \(\varphi\) and \(s\) satisfies \(\mathsf{EX}\,\mathsf{EG}\,\varphi\), that is, some successor of \(s\) satisfies \(\mathsf{EG}\,\varphi\).

Both directions are direct manipulations of infinite runs; no choice is needed.

theorem existsGlobally_expansion :
    Satisfies lts valuation s (.existsGlobally φ) ↔
      Satisfies lts valuation s φ ∧
        Satisfies lts valuation s (.existsNext (.existsGlobally φ))

Uses 4 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas

Proof usesInfinite run · Shifted sequence

Used by\(\mathsf{EG}\) is a greatest fixed point

DefinitionThe \(\mathsf{EF}\) functional#✓fully proved

Given a labelled transition system, a valuation of the atoms at its states, and a CTL formula \(\varphi\), this is the map sending a set of states \(Z\) to the set of states that satisfy \(\varphi\) or have some successor in \(Z\).

Its least fixed point is the set of states satisfying \(\mathsf{EF}\,\varphi\).

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

Uses 3 · Used by 1

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

Used byThe \(\mathsf{EF}\) operator

DefinitionThe \(\mathsf{EF}\) operator#✓fully proved

Given a labelled transition system, a valuation of the atoms at its states, and a CTL formula \(\varphi\), this is the monotone operator on sets of states, ordered by inclusion, sending a set \(Z\) to the set of states that satisfy \(\varphi\) or have some successor in \(Z\).

def existsFinallyOrderHom (lts : LTS State Label)
    (valuation : State → Atom → Prop) (φ : Formula Atom) :
    (State → Prop) →o (State → Prop) :=
  ⟨existsFinallyFun lts valuation φ, existsFinallyFun_mono lts valuation φ⟩

Uses 4 · Used by 1

Statement usesCTL formulas · Existential predecessor operator · Satisfaction of CTL formulas · The \(\mathsf{EF}\) functional

Used by\(\mathsf{EF}\) is a least fixed point

DefinitionThe functional for \(\mathrm{EG}\)#✓fully proved

Given a labelled transition system, a valuation of the atoms and a CTL formula \(\varphi\), this is the operator that sends a predicate \(Z\) on states to the predicate holding at a state \(s\) when \(s\) satisfies \(\varphi\) and some successor of \(s\) satisfies \(Z\), that is, there are a label \(a\) and a state \(t\) with a transition from \(s\) to \(t\) labelled \(a\) such that \(Z\) holds at \(t\).

Its greatest fixed point is the set of states satisfying \(\mathrm{EG}\,\varphi\).

def existsGloballyFun (lts : LTS State Label)
    (valuation : State → Atom → Prop) (φ : Formula Atom)
    (Z : State → Prop) : State → Prop :=
  fun 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 \(\mathrm{EG}\) functional as a monotone operator · Correctness of the finite fixed-point computation of EG

DefinitionThe \(\mathrm{EG}\) functional as a monotone operator#✓fully proved

Given a labelled transition system, a valuation of the atoms and a CTL formula \(\varphi\), this is the monotone map on predicates on states, ordered pointwise by implication, that sends a predicate \(Z\) to the predicate holding at a state \(s\) when \(s\) satisfies \(\varphi\) and some successor of \(s\) satisfies \(Z\).

def existsGloballyOrderHom (lts : LTS State Label)
    (valuation : State → Atom → Prop) (φ : Formula Atom) :
    (State → Prop) →o (State → Prop) :=
  ⟨existsGloballyFun lts valuation φ, existsGloballyFun_mono lts valuation φ⟩

Uses 4 · Used by 2

Statement usesCTL formulas · Existential predecessor operator · Satisfaction of CTL formulas · The functional for \(\mathrm{EG}\)

Used by\(\mathsf{EG}\) is a greatest fixed point · Correctness of the finite fixed-point computation of EG

Theorem\(\mathsf{EF}\) is a least fixed point#✓fully proved

Fix a labelled transition system, a valuation of the atoms at its states, and a CTL formula \(\varphi\). Write \([\![\varphi]\!]\) for the set of states satisfying \(\varphi\) and \(\mathrm{Pre}_\exists(Z)\) for the set of states having some successor in a set of states \(Z\). Then the set of states satisfying \(\mathsf{EF}\,\varphi\) is the least fixed point of the monotone operator \(Z \mapsto [\![\varphi]\!] \cup \mathrm{Pre}_\exists(Z)\) on sets of states.

The fixed point is contained in \(\mathsf{EF}\,\varphi\) by Park induction, using the one-step expansion of \(\mathsf{EF}\); the converse is induction on a path to a \(\varphi\)-state, unfolding the fixed point once per step.

theorem existsFinally_eq_lfp (φ : Formula Atom) :
    (fun s => Satisfies lts valuation s φ.existsFinally) =
      (existsFinallyOrderHom lts valuation φ).lfp

Uses 7

Statement usesCTL formulas · Exists finally · Satisfaction of CTL formulas · The \(\mathsf{EF}\) operator

Proof usesExistential predecessor operator · One-step expansion of \(\mathsf{EF}\) · \(\mathsf{EF}\) means reachability

Theorem\(\mathsf{EG}\) is a greatest fixed point#✓fully proved

Fix a labelled transition system, a valuation of the atoms at its states, and a CTL formula \(\varphi\). Write \([\![\varphi]\!]\) for the set of states satisfying \(\varphi\) and \(\mathrm{Pre}_\exists(Z)\) for the set of states having some successor in a set of states \(Z\). Then the set of states satisfying \(\mathsf{EG}\,\varphi\) is the greatest fixed point of the monotone operator \(Z \mapsto [\![\varphi]\!] \cap \mathrm{Pre}_\exists(Z)\) on sets of states.

The inclusion of \(\mathsf{EG}\,\varphi\) in the fixed point is coinduction, using the one-step expansion of \(\mathsf{EG}\). The converse builds an infinite run by repeatedly choosing a successor inside the fixed point, so it uses the axiom of choice.

theorem existsGlobally_eq_gfp (φ : Formula Atom) :
    (fun s => Satisfies lts valuation s (.existsGlobally φ)) =
      (existsGloballyOrderHom lts valuation φ).gfp

Uses 5 · Used by 1

Statement usesCTL formulas · Satisfaction of CTL formulas · The \(\mathrm{EG}\) functional as a monotone operator

Proof usesOne-step expansion of \(\mathsf{EG}\) · Infinite run

Used byCorrectness of the finite fixed-point computation of EG

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.