Model checking for linear temporal logic

DefinitionTruth-annotation states of the LTL tableau#✓fully proved

One Boolean for each syntactic occurrence in an LTL formula.

@[reducible]
def State : Formula Atom → Type
  | .atom _ => Bool
  | .top => Bool
  | .not φ => Bool × State φ
  | .and φ ψ => Bool × (State φ × State ψ)
  | .next φ => Bool × State φ
  | .until φ ψ => Bool × (State φ × State ψ)
Uses 1 · Used by 22
Statement usesFormulas of linear temporal logic
Used byComputable fairness-counter update · Generalized Büchi tableau for an LTL formula · Büchi automaton for an LTL formula · Büchi transition test via the computable counter update · Executable full-LTL model checker · Correctness of the executable LTL model checker · Counterexample product for an LTL formula · Every LTL formula has a finite-state Büchi automaton · Fairness of a tableau annotation sequence · Tableau fairness is generalized Büchi acceptance · Generalized LTL tableau language equals the formula language · Büchi automaton language equals the LTL formula language · LTL tableau accepts exactly the satisfying words · Büchi automaton accepts exactly the satisfying words · Counterexample words are runs violating the formula · Tableau acceptance via initial, local and fairness conditions · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso · Computable counter update equals generic degeneralization · Boolean test for an until fairness obligation · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation

DefinitionRoot truth bit of a tableau annotation#✓fully proved

The truth bit at the root of an annotation.

def value : (φ : Formula Atom) → State φ → Bool
  | .atom _, s => s
  | .top, s => s
  | .not _, s => s.1
  | .and _ _, s => s.1
  | .next _, s => s.1
  | .until _ _, s => s.1
Uses 2 · Used by 9
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau
Used byGeneralized Büchi tableau for an LTL formula · Executable full-LTL model checker · Correctness of the executable LTL model checker · Fairness of a tableau annotation sequence · Tableau fairness is generalized Büchi acceptance · LTL tableau accepts exactly the satisfying words · Tableau acceptance via initial, local and fairness conditions · Boolean test for an until fairness obligation · Local transition relation of the LTL tableau

DefinitionNumber of until fairness obligations#✓fully proved

The number of until occurrences, hence of fairness requirements.

def obligationCount : Formula Atom → ℕ
  | .atom _ => 0
  | .top => 0
  | .not φ => obligationCount φ
  | .and φ ψ => obligationCount φ + obligationCount ψ
  | .next φ => obligationCount φ
  | .until φ ψ => obligationCount φ + obligationCount ψ + 1
Uses 1 · Used by 17
Statement usesFormulas of linear temporal logic
Used byComputable fairness-counter update · Generalized Büchi tableau for an LTL formula · Büchi automaton for an LTL formula · Büchi transition test via the computable counter update · Executable full-LTL model checker · Correctness of the executable LTL model checker · Counterexample product for an LTL formula · Every LTL formula has a finite-state Büchi automaton · Tableau fairness is generalized Büchi acceptance · Büchi automaton language equals the LTL formula language · Büchi automaton accepts exactly the satisfying words · Counterexample words are runs violating the formula · Tableau acceptance via initial, local and fairness conditions · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso · Computable counter update equals generic degeneralization · Boolean test for an until fairness obligation

DefinitionLocal transition relation of the LTL tableau#✓fully proved

Local equations at every occurrence. The symbol labels the source state.

Cslib.LTL.Tableau.step · 19 lines 
def step (valuation : Symbol → Atom → Prop) :
    (φ : Formula Atom) → State φ → Symbol → State φ → Prop
  | .atom a, s, x, _ => s = true ↔ valuation x a
  | .top, s, _, _ => s = true
  | .not φ, s, x, t =>
      (s.1 = true ↔ ¬ value φ s.2 = true) ∧
        step valuation φ s.2 x t.2
  | .and φ ψ, s, x, t =>
      (s.1 = true ↔ value φ s.2.1 = true ∧ value ψ s.2.2 = true) ∧
        step valuation φ s.2.1 x t.2.1 ∧
        step valuation ψ s.2.2 x t.2.2
  | .next φ, s, x, t =>
      (s.1 = true ↔ value φ t.2 = true) ∧
        step valuation φ s.2 x t.2
  | .until φ ψ, s, x, t =>
      (s.1 = true ↔ value ψ s.2.2 = true ∨
        (value φ s.2.1 = true ∧ t.1 = true)) ∧
        step valuation φ s.2.1 x t.2.1 ∧
        step valuation ψ s.2.2 x t.2.2
Uses 3 · Used by 6
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Root truth bit of a tableau annotation
Used byGeneralized Büchi tableau for an LTL formula · Büchi transition test via the computable counter update · Executable full-LTL model checker · Correctness of the executable LTL model checker · LTL tableau accepts exactly the satisfying words · Tableau acceptance via initial, local and fairness conditions

DefinitionBoolean test for an until fairness obligation#✓fully proved

The Boolean test for each until fairness requirement.

def obligation : (φ : Formula Atom) →
    Fin (obligationCount φ) → State φ → Bool
  | .atom _, i, _ => Fin.elim0 i
  | .top, i, _ => Fin.elim0 i
  | .not φ, i, s => obligation φ i s.2
  | .and φ ψ, i, s =>
      Fin.addCases (fun j => obligation φ j s.2.1)
        (fun j => obligation ψ j s.2.2) i
  | .next φ, i, s => obligation φ i s.2
  | .until φ ψ, i, s =>
      Fin.cases (!s.1 || value ψ s.2.2)
        (Fin.addCases (fun j => obligation φ j s.2.1)
          (fun j => obligation ψ j s.2.2)) i
Uses 4 · Used by 5
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Number of until fairness obligations · Root truth bit of a tableau annotation
Used byComputable fairness-counter update · Generalized Büchi tableau for an LTL formula · Tableau fairness is generalized Büchi acceptance · Tableau acceptance via initial, local and fairness conditions · Computable counter update equals generic degeneralization

DefinitionFairness of a tableau annotation sequence#✓fully proved

Every until occurrence is absent or fulfilled at arbitrarily late times.

def Fair : (φ : Formula Atom) → ωSequence (State φ) → Prop
  | .atom _, _ => True
  | .top, _ => True
  | .not φ, ss => Fair φ (fun n => (ss n).2)
  | .and φ ψ, ss =>
      Fair φ (fun n => (ss n).2.1) ∧ Fair ψ (fun n => (ss n).2.2)
  | .next φ, ss => Fair φ (fun n => (ss n).2)
  | .until φ ψ, ss =>
      (∃ᶠ n in atTop, (ss n).1 = false ∨ value ψ (ss n).2.2 = true) ∧
        Fair φ (fun n => (ss n).2.1) ∧ Fair ψ (fun n => (ss n).2.2)
Uses 3 · Used by 3
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Root truth bit of a tableau annotation
Used byTableau fairness is generalized Büchi acceptance · LTL tableau accepts exactly the satisfying words · Tableau acceptance via initial, local and fairness conditions

DefinitionGeneralized Büchi tableau for an LTL formula#✓fully proved

Generalized Büchi tableau: the root is initially true.

def automaton (valuation : Symbol → Atom → Prop) (φ : Formula Atom) :
    Automata.NA.GenBuchi (State φ) Symbol where
  Tr := step valuation φ
  start := {s | value φ s = true}
  k := obligationCount φ
  accept i := {s | obligation φ i s = true}
Uses 7 · Used by 7
Statement usesGeneralized Büchi automaton · Formulas of linear temporal logic · Truth-annotation states of the LTL tableau · Boolean test for an until fairness obligation · Number of until fairness obligations · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation
Used byBüchi automaton for an LTL formula · Büchi transition test via the computable counter update · Generalized LTL tableau language equals the formula language · Büchi automaton language equals the LTL formula language · LTL tableau accepts exactly the satisfying words · Tableau acceptance via initial, local and fairness conditions · Computable counter update equals generic degeneralization

TheoremTableau fairness is generalized Büchi acceptance#✓fully proved

Structural fairness is exactly generalized Büchi acceptance.

theorem fair_iff (φ : Formula Atom) (ss : ωSequence (State φ)) :
    Fair φ ss ↔ ∀ i, ∃ᶠ n in atTop, obligation φ i (ss n) = true
Uses 6 · Used by 1
Statement usesFormulas of linear temporal logic · Fairness of a tableau annotation sequence · Truth-annotation states of the LTL tableau · Boolean test for an until fairness obligation · Number of until fairness obligations
Proof usesRoot truth bit of a tableau annotation
Used byTableau acceptance via initial, local and fairness conditions

TheoremTableau acceptance via initial, local and fairness conditions#✓fully proved

Membership exposes exactly the initial, local, and fairness conditions.

theorem mem_language_iff (valuation : Symbol → Atom → Prop)
    (φ : Formula Atom) (w : ωSequence Symbol) :
    w ∈ language (automaton valuation φ) ↔
      ∃ ss : ωSequence (State φ), value φ (ss 0) = true ∧
        (∀ n, step valuation φ (ss n) (w n) (ss (n + 1))) ∧
        Fair φ ss
Uses 11 · Used by 1
Statement usesGeneralized Büchi automaton · Formulas of linear temporal logic · Fairness of a tableau annotation sequence · Truth-annotation states of the LTL tableau · Generalized Büchi tableau for an LTL formula · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation
Proof usesLanguage of a generalized Büchi automaton · Tableau fairness is generalized Büchi acceptance · Boolean test for an until fairness obligation · Number of until fairness obligations
Used byLTL tableau accepts exactly the satisfying words

TheoremLTL tableau accepts exactly the satisfying words#✓fully proved

The full tableau recognizes exactly the existing LTL satisfaction relation.

theorem mem_automaton_iff (valuation : Symbol → Atom → Prop)
    (φ : Formula Atom) (w : ωSequence Symbol) :
    w ∈ language (automaton valuation φ) ↔ Word.Satisfies valuation w φ
Uses 13 · Used by 1
Statement usesGeneralized Büchi automaton · Formulas of linear temporal logic · Truth-annotation states of the LTL tableau · Generalized Büchi tableau for an LTL formula · Satisfaction of LTL formulas on ω-words
Proof usesFairness of a tableau annotation sequence · Tableau acceptance via initial, local and fairness conditions · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation · Expansion law for until · Satisfaction at a position · Satisfaction of an atom at a position · Satisfaction on a suffix
Used byGeneralized LTL tableau language equals the formula language

TheoremGeneralized LTL tableau language equals the formula language#✓fully proved

Exact omega-language equality for the generalized tableau.

theorem language_automaton (valuation : Symbol → Atom → Prop) (φ : Formula Atom) :
    language (automaton valuation φ) = Word.language valuation φ
Uses 6 · Used by 1
Statement usesGeneralized Büchi automaton · Formulas of linear temporal logic · Truth-annotation states of the LTL tableau · Generalized Büchi tableau for an LTL formula · Language of an LTL formula
Proof usesLTL tableau accepts exactly the satisfying words
Used byBüchi automaton language equals the LTL formula language

DefinitionBüchi automaton for an LTL formula#✓fully proved

Ordinary Büchi recognition, using the existing fairness counter.

def buchi (valuation : Symbol → Atom → Prop) (φ : Formula Atom) :
    Automata.NA.Buchi (State φ × Fin (obligationCount φ + 1)) Symbol :=
  (automaton valuation φ).toBuchi
Uses 5 · Used by 8
Statement usesDegeneralization of a generalized Büchi automaton · Formulas of linear temporal logic · Truth-annotation states of the LTL tableau · Generalized Büchi tableau for an LTL formula · Number of until fairness obligations
Used byBüchi transition test via the computable counter update · Executable full-LTL model checker · Correctness of the executable LTL model checker · Counterexample product for an LTL formula · Every LTL formula has a finite-state Büchi automaton · Büchi automaton language equals the LTL formula language · Büchi automaton accepts exactly the satisfying words · Counterexample words are runs violating the formula

TheoremBüchi automaton language equals the LTL formula language#✓fully proved

Every LTL formula has precisely its existing language as a Büchi language.

theorem language_buchi (valuation : Symbol → Atom → Prop) (φ : Formula Atom) :
    language (buchi valuation φ) = Word.language valuation φ
Uses 10 · Used by 2
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Büchi automaton for an LTL formula · Number of until fairness obligations · Language of an LTL formula
Proof usesGeneralized Büchi automaton · Degeneralization preserves the language · Degeneralization of a generalized Büchi automaton · Generalized Büchi tableau for an LTL formula · Generalized LTL tableau language equals the formula language
Used byEvery LTL formula has a finite-state Büchi automaton · Büchi automaton accepts exactly the satisfying words

TheoremBüchi automaton accepts exactly the satisfying words#✓fully proved

The ordinary Büchi recognizer accepts exactly satisfaction of the formula.

theorem mem_buchi_iff (valuation : Symbol → Atom → Prop)
    (φ : Formula Atom) (w : ωSequence Symbol) :
    w ∈ language (buchi valuation φ) ↔ Word.Satisfies valuation w φ
Uses 8 · Used by 1
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Büchi automaton for an LTL formula · Number of until fairness obligations · Satisfaction of LTL formulas on ω-words
Proof usesBüchi automaton language equals the LTL formula language · Language of an LTL formula · Membership in the language of a formula
Used byCounterexample words are runs violating the formula

TheoremEvery LTL formula has a finite-state Büchi automaton#✓fully proved

Every existing LTL formula has a finite-state Büchi recognizer under the same valuation. Neither atoms nor the alphabet need be finite or decidable.

theorem exists_buchi (valuation : Symbol → Atom → Prop) (φ : Formula Atom) :
    ∃ (S : Type) (_ : Finite S) (a : Automata.NA.Buchi S Symbol),
      language a = Word.language valuation φ
Uses 6
Statement usesFormulas of linear temporal logic · Language of an LTL formula
Proof usesTruth-annotation states of the LTL tableau · Büchi automaton for an LTL formula · Büchi automaton language equals the LTL formula language · Number of until fairness obligations

DefinitionInitial infinite run of a transition system#✓fully proved

An initial infinite state run, witnessed by a canonical action execution.

def IsRun (lts : LTS State Action) (initial : Set State)
    (w : ωSequence State) : Prop :=
  w 0 ∈ initial ∧ ∃ actions : ωSequence Action, lts.OmegaExecution w actions
Used by 6
Used byRuns are sequences with a transition between adjacent states · Counterexample words are runs violating the formula · Product accepts exactly the runs accepted by the recognizer · Satisfaction of an LTL formula by all initial runs · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso

TheoremRuns are sequences with a transition between adjacent states#✓fully proved

Equivalently, every adjacent state pair has a real model transition.

theorem isRun_iff (lts : LTS State Action) (initial : Set State)
    (w : ωSequence State) :
    IsRun lts initial w ↔ w 0 ∈ initial ∧
      ∀ n, ∃ action, lts.Tr (w n) action (w (n + 1))
Uses 1 · Used by 1
Statement usesInitial infinite run of a transition system
Used byProduct accepts exactly the runs accepted by the recognizer

DefinitionProduct of a transition system with a Büchi recognizer#✓fully proved

Synchronized state-reading product, with the recognizer's Büchi condition.

def product (lts : LTS State Action) (initial : Set State)
    (a : Buchi Q State) : Buchi (State × Q) State where
  Tr p x q := x = p.1 ∧ (∃ action, lts.Tr p.1 action q.1) ∧ a.Tr p.2 x q.2
  start := {p | p.1 ∈ initial ∧ p.2 ∈ a.start}
  accept := {p | p.2 ∈ a.accept}
Used by 5
Used byExecutable full-LTL model checker · Correctness of the executable LTL model checker · Counterexample product for an LTL formula · Counterexample words are runs violating the formula · Product accepts exactly the runs accepted by the recognizer

TheoremProduct accepts exactly the runs accepted by the recognizer#✓fully proved

A product accepts precisely the model runs accepted by its recognizer.

theorem mem_product_iff (lts : LTS State Action) (initial : Set State)
    (a : Buchi Q State) (w : ωSequence State) :
    w ∈ language (product lts initial a) ↔ IsRun lts initial w ∧ w ∈ language a
Uses 3 · Used by 1
Statement usesInitial infinite run of a transition system · Product of a transition system with a Büchi recognizer
Proof usesRuns are sequences with a transition between adjacent states
Used byCounterexample words are runs violating the formula

DefinitionCounterexample product for an LTL formula#✓fully proved

The finite-state product for runs that violate the full LTL formula.

def counterexample (lts : LTS State Action) (initial : Set State)
    (valuation : State → Atom → Prop) (φ : Formula Atom) :
    Buchi (State × (Tableau.State (.not φ) ×
      Fin (Tableau.obligationCount (.not φ) + 1))) State :=
  product lts initial (Tableau.buchi valuation (.not φ))
Uses 5 · Used by 4
Statement usesFormulas of linear temporal logic · Product of a transition system with a Büchi recognizer · Truth-annotation states of the LTL tableau · Büchi automaton for an LTL formula · Number of until fairness obligations
Used byCorrectness of the executable LTL model checker · Counterexample words are runs violating the formula · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso

DefinitionSatisfaction of an LTL formula by all initial runs#✓fully proved

All initial infinite canonical executions satisfy the formula.

def Models (lts : LTS State Action) (initial : Set State)
    (valuation : State → Atom → Prop) (φ : Formula Atom) : Prop :=
  ∀ w : ωSequence State, IsRun lts initial w → Word.Satisfies valuation w φ
Uses 3 · Used by 3
Statement usesFormulas of linear temporal logic · Initial infinite run of a transition system · Satisfaction of LTL formulas on ω-words
Used byCorrectness of the executable LTL model checker · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso

TheoremCounterexample words are runs violating the formula#✓fully proved

A counterexample word is exactly an infinite model run violating LTL.

theorem mem_counterexample_iff (lts : LTS State Action) (initial : Set State)
    (valuation : State → Atom → Prop) (φ : Formula Atom) (w : ωSequence State) :
    w ∈ language (counterexample lts initial valuation φ) ↔
      IsRun lts initial w ∧ ¬ Word.Satisfies valuation w φ
Uses 10 · Used by 2
Statement usesFormulas of linear temporal logic · Initial infinite run of a transition system · Counterexample product for an LTL formula · Truth-annotation states of the LTL tableau · Number of until fairness obligations · Satisfaction of LTL formulas on ω-words
Proof usesProduct accepts exactly the runs accepted by the recognizer · Product of a transition system with a Büchi recognizer · Büchi automaton for an LTL formula · Büchi automaton accepts exactly the satisfying words
Used byLTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso

TheoremFinite-model LTL satisfaction iff no counterexample lasso#✓fully proved

Full-LTL model checking reduces to the proved finite Büchi lasso criterion. A cycle must be nonempty; neither seriality nor finite action/atom types are needed.

theorem models_iff_no_lasso [Finite State] (lts : LTS State Action)
    (initial : Set State) (valuation : State → Atom → Prop) (φ : Formula Atom) :
    Models lts initial valuation φ ↔
      ¬ (counterexample lts initial valuation φ).HasLasso
Uses 10
Statement usesLasso of a Büchi automaton · Formulas of linear temporal logic · Satisfaction of an LTL formula by all initial runs · Counterexample product for an LTL formula · Truth-annotation states of the LTL tableau · Number of until fairness obligations
Proof usesLasso characterization of Büchi nonemptiness · Initial infinite run of a transition system · Counterexample words are runs violating the formula · Satisfaction of LTL formulas on ω-words

TheoremLTL satisfaction iff the counterexample language is empty#✓fully proved

Universal infinite-run satisfaction is emptiness of the counterexample language.

theorem models_iff_language_empty (lts : LTS State Action) (initial : Set State)
    (valuation : State → Atom → Prop) (φ : Formula Atom) :
    Models lts initial valuation φ ↔
      language (counterexample lts initial valuation φ) = ⊥
Uses 8 · Used by 1
Statement usesFormulas of linear temporal logic · Satisfaction of an LTL formula by all initial runs · Counterexample product for an LTL formula · Truth-annotation states of the LTL tableau · Number of until fairness obligations
Proof usesInitial infinite run of a transition system · Counterexample words are runs violating the formula · Satisfaction of LTL formulas on ω-words
Used byCorrectness of the executable LTL model checker

DefinitionComputable fairness-counter update#✓fully proved

Computable fairness-counter update, reading the destination annotation.

def advance (φ : Formula Atom) (i : Fin (obligationCount φ + 1)) (t : State φ) :
    Fin (obligationCount φ + 1) :=
  if h : i.val < obligationCount φ then
    if obligation φ ⟨i.val, h⟩ t = true then ⟨i.val + 1, by omega⟩ else i
  else ⟨0, Nat.zero_lt_succ _⟩
Uses 4 · Used by 4
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Boolean test for an until fairness obligation · Number of until fairness obligations
Used byBüchi transition test via the computable counter update · Executable full-LTL model checker · Correctness of the executable LTL model checker · Computable counter update equals generic degeneralization

TheoremComputable counter update equals generic degeneralization#✓fully proved

The computable update is exactly the existing generic degeneralization.

theorem nextCount_eq_advance (valuation : Symbol → Atom → Prop) (φ : Formula Atom)
    (i : Fin (obligationCount φ + 1)) (t : State φ) :
    (automaton valuation φ).nextCount i t = advance φ i t
Uses 8 · Used by 1
Statement usesGeneralized Büchi automaton · Counter update for degeneralization · Formulas of linear temporal logic · Truth-annotation states of the LTL tableau · Computable fairness-counter update · Generalized Büchi tableau for an LTL formula · Number of until fairness obligations
Proof usesBoolean test for an until fairness obligation
Used byBüchi transition test via the computable counter update

TheoremBüchi transition test via the computable counter update#✓fully proved

The existing Büchi transition can be tested using the computable update.

theorem buchi_tr_iff (valuation : Symbol → Atom → Prop) (φ : Formula Atom)
    (p : State φ × Fin (obligationCount φ + 1)) (x : Symbol)
    (q : State φ × Fin (obligationCount φ + 1)) :
    (buchi valuation φ).Tr p x q ↔
      step valuation φ p.1 x q.1 ∧ q.2 = advance φ p.2 q.1
Uses 10 · Used by 2
Statement usesFormulas of linear temporal logic · Truth-annotation states of the LTL tableau · Computable fairness-counter update · Büchi automaton for an LTL formula · Number of until fairness obligations · Local transition relation of the LTL tableau
Proof usesGeneralized Büchi automaton · Counter update for degeneralization · Generalized Büchi tableau for an LTL formula · Computable counter update equals generic degeneralization
Used byExecutable full-LTL model checker · Correctness of the executable LTL model checker

DefinitionExecutable full-LTL model checker#✓fully proved

Full-LTL checking by the existing finite Büchi reachability algorithm. The finite/decidable data requirements are only for execution, not recognition.

def checkB : Bool := by
  letI : DecidablePred (· ∈ (Tableau.buchi valuation (.not φ)).start) :=
    Tableau.buchiStartDecidable valuation (.not φ)
  letI : DecidablePred (· ∈ (Tableau.buchi valuation (.not φ)).accept) :=
    Tableau.buchiAcceptDecidable valuation (.not φ)
  exact (product lts initial (Tableau.buchi valuation (.not φ))).isEmptyB
Uses 10 · Used by 1
Statement usesBüchi emptiness test · Formulas of linear temporal logic · Product of a transition system with a Büchi recognizer · Truth-annotation states of the LTL tableau · Computable fairness-counter update · Büchi automaton for an LTL formula · Büchi transition test via the computable counter update · Number of until fairness obligations · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation
Used byCorrectness of the executable LTL model checker

TheoremCorrectness of the executable LTL model checker#✓fully proved

The executable checker is correct for all initial infinite model runs.

theorem checkB_iff :
    checkB lts initial valuation φ = true ↔ Models lts initial valuation φ
Uses 15
Statement usesFormulas of linear temporal logic · Satisfaction of an LTL formula by all initial runs · Executable full-LTL model checker
Proof usesBüchi emptiness test · Correctness of the Büchi emptiness test · Counterexample product for an LTL formula · LTL satisfaction iff the counterexample language is empty · Product of a transition system with a Büchi recognizer · Truth-annotation states of the LTL tableau · Computable fairness-counter update · Büchi automaton for an LTL formula · Büchi transition test via the computable counter update · Number of until fairness obligations · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation
29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.