Linear Temporal Logic and Büchi automata

We define the syntax and language of Linear Temporal Logic (LTL) formulas and of nondeterministic Büchi automata (NBW), and state the theorem that every LTL formula has an equivalent finite-state NBW.

inductive LeanModelChecking.LTL (AP : Type) : Type

A Linear Temporal Logic formula.

• atom {AP : Type} (p : AP) : LTL AP
• not {AP : Type} (φ : LTL AP) : LTL AP
• or {AP : Type} (φ₁ φ₂ : LTL AP) : LTL AP
• next {AP : Type} (φ : LTL AP) : LTL AP
• until {AP : Type} (φ₁ φ₂ : LTL AP) : LTL AP

@[reducible, inline]

abbrev LeanModelChecking.Letter (AP : Type) : Type

A letter is a set of atomic propositions.

Equations

• LeanModelChecking.Letter AP = Set AP

def LeanModelChecking.LTL.language {AP : Type} (f : LTL AP) (w : ℕ → Letter AP) : Prop

The language of a Linear Temporal Logic formula, defined as a predicate over a word.

Equations

• (LeanModelChecking.LTL.atom p).language w = (p ∈ w 0)
• φ.not.language w = ¬φ.language w
• (φ₁.or φ₂).language w = (φ₁.language w ∨ φ₂.language w)
• φ.next.language w = φ.language fun (j : ℕ) => w (j + 1)
• (φ₁.until φ₂).language w = ∃ (i : ℕ), (φ₂.language fun (j : ℕ) => w (j + i)) ∧ ∀ (k : ℕ), k < i → φ₁.language fun (j : ℕ) => w (j + k)

structure LeanModelChecking.NBW (S : Type) : Type 1

A Büchi automaton, on some letter type S.

• Q : Type

  The type of states.

• q₀ : Set self.Q

  The set of starting states.

• δ : self.Q → S → self.Q → Prop

  The transition relation.

• F : Set self.Q

  The set of accepting states. A run is accepting if it visits states in F infinitely often.

def LeanModelChecking.NBW.run {S : Type} (A : NBW S) (p : ℕ → A.Q) (w : ℕ → S) : Prop

Whether the sequence of states p is a run on the word w on the Büchi automaton A.

Equations

• A.run p w = (p 0 ∈ A.q₀ ∧ ∀ (i : ℕ), A.δ (p i) (w i) (p (i + 1)))

def LeanModelChecking.NBW.language {S : Type} (A : NBW S) (w : ℕ → S) : Prop

The language of a Büchi automaton, defined as a predicate over a word.

Equations

• A.language w = ∃ (p : ℕ → A.Q), A.run p w ∧ ∀ (i : ℕ), ∃ (j : ℕ), j ≥ i ∧ p j ∈ A.F

def LeanModelChecking.forAnyLTLFormulaExistsAnEquivalentNBWStatement : Prop

The statement that every Linear Temporal Logic formula has an equivalent finite-state nondeterministic Büchi automaton, packaged as a proposition so it can be reused. Without the Finite A.Q conjunct the statement would be much weaker, since an automaton with infinitely many states can encode arbitrary languages.

Equations

• One or more equations did not get rendered due to their size.