Linear Temporal Logic to Büchi automata translation

Stream: CSLib

[György Kurucz]

I have formalized the LTL -> Büchi automaton translation (going through Alternating Büchi automata), haven't seen this done in Lean yet, it came out at around ~2300 lines: https://github.com/kuruczgy/lean-model-checking/

Here is the theorem statement (if you spot any errors let me know):

import Mathlib.Data.Set.Basic
import Mathlib.Data.Finite.Defs

/-- A Linear Temporal Logic formula. -/
inductive LTL (AP : Type) where
| atom (p : AP)
| not (φ : LTL AP)
| or (φ₁ φ₂ : LTL AP)
| next (φ : LTL AP)
| until (φ₁ φ₂ : LTL AP)

/-- A letter is a set of atomic propositions. -/
abbrev Letter (AP : Type) := Set AP

/-- The language of a Linear Temporal Logic formula,
defined as a predicate over a word. -/
def LTL.language {AP} (f : LTL AP) (w : ℕ → Letter AP) : Prop :=
  match f with
  | .atom p => p ∈ w 0
  | .not φ => ¬language φ w
  | .or φ₁ φ₂ => language φ₁ w ∨ language φ₂ w
  | .next φ => language φ (fun j => w (j + 1))
  | .until φ₁ φ₂ =>
    ∃ i, language φ₂ (fun j => w (j + i)) ∧
    ∀ k < i, language φ₁ (fun j => w (j + k))

/-- A Büchi automaton, on some letter type `S`. -/
structure NBW (S : Type) where
  /-- The type of states. -/
  Q : Type
  /-- The set of starting states. -/
  q₀ : Set Q
  /-- The transition relation. -/
  δ : Q → S → Q → Prop
  /-- The set of accepting states. A run is accepting
  if it visits states in `F` infinitely often. -/
  F : Set Q

/-- Whether the sequence of states `p` is a run on the
word `w` on the Büchi automaton `A`. -/
def NBW.run {S} (A : NBW S) (p : ℕ → A.Q) (w : ℕ → S) :=
  p 0 ∈ A.q₀ ∧ ∀ i, A.δ (p i) (w i) (p (i + 1))

/-- The language of a Büchi automaton,
defined as a predicate over a word. -/
def NBW.language {S} (A : NBW S) (w : ℕ → S) :=
  ∃ p, A.run p w ∧ ∀ i, ∃ j ≥ i, p j ∈ A.F

def for_any_LTL_formula_exists_an_equivalent_NBW_statement :=
  ∀ {AP} (φ : LTL AP), ∃ (A : NBW (Letter AP)), φ.language = A.language

[Ching-Tsun Chou]

Buchi automata and some properties of ω-regular languages are already in cslib:
https://github.com/leanprover/cslib/blob/main/Cslib/Computability/Automata/NA/Basic.lean
https://github.com/leanprover/cslib/blob/main/Cslib/Computability/Languages/OmegaRegularLanguage.lean
But alternating automata, LTL, and their relationship would be very valuable additions to cslib.

[Chris Henson]

There is also a recent project for formalizing LTLs in Lean: repo, paper, talk

[György Kurucz]

For inclusion in cslib I think some thought would have to be put into how to best formulate alternating automata. This is my current formulation:

inductive PositiveBool (Q : Type) where
| atom (q : Q)
| true
| false
| and (ψ₁ ψ₂ : PositiveBool Q)
| or (ψ₁ ψ₂ : PositiveBool Q)

def PositiveBool.Sat {Q} (Y : Set Q) : PositiveBool Q → Prop
| atom q => q ∈ Y
| true => True
| false => False
| and ψ₁ ψ₂ => Sat Y ψ₁ ∧ Sat Y ψ₂
| or ψ₁ ψ₂ => Sat Y ψ₁ ∨ Sat Y ψ₂

structure ABW (S Q : Type) where
  q₀ : Q
  δ : Q → S → PositiveBool Q
  F : Set Q

structure DAG Q where
  V : Set (Q × ℕ)
  E : Set ((Q × ℕ) × Q)
  edge_closure: ∀ e ∈ E, e.1 ∈ V ∧ (e.2, e.1.2 + 1) ∈ V

def DAG.path {Q} (G : DAG Q) (p : ℕ → Q) :=
  ∃ n, ∀ i, ((p i, n + i), p (i + 1)) ∈ G.E

structure RunDAG {S Q} (A : ABW S Q) (w : ℕ → S) extends DAG Q where
  p_root : (A.q₀, 0) ∈ V
  p_sat :
    ∀ v ∈ V, let (q, i) := v;
    ∃ Y,
    PositiveBool.Sat Y (A.δ q (w i)) ∧
    {(q, i)} ×ˢ Y ⊆ E

def RunDAG.accepting {S Q} {A : ABW S Q} {w : ℕ → S} (G : RunDAG A w) :=
  ∀ p, G.path p → ∀ i, ∃ j ≥ i, p j ∈ A.F

def ABW.language {S Q} (A : ABW S Q) (w : Nat → S) :=
  ∃ (G : RunDAG A w), G.accepting

• Do we want to use positive boolean formulas? The isabelle proof I saw used conjunctive normal forms.
• The transition function delta does not fit the current LTS state transition relation type.
• We probably want run trees for not-memoryless alternating automata (not sure which ones those are), but also run DAGs for better proofs. Not sure what's an elegant formalism for either of these. (Do we want to define the DAG as an actual DAG connected to some existing graph theory definitions, or just define it separately like I did here.)

[Ching-Tsun Chou]

I think what you call "run DAGs" are really "run trees", right? It seems to me that before getting into the nitty-gritty of alternating automata, you need to develop the theories of finite and infinite run trees. The current automata theory in cslib is built on top of the theories of List (for finite runs) and ωSequence (for infinite runs). The counterparts of these theories for alternating automata are finite and infinite run trees.

I doubt the current LTS theory in cslib would be of much use, because it is very much tailored for a linear notion of execution. I don't know whether there is a notion of "alternating LTS". Perhaps @Fabrizio Montesi knows?

[Ching-Tsun Chou]

After thinking more about it, I think DAG is indeed required, because one can imagine defining analogues like List.drop or ωSequence.drop, which in general will produce a DAG even if one starts with a tree. On the other hand, I don't think the notion of general DAGs is appropriate here either, because the DAGs used to model the executions of alternating automata are naturally "layered" by time and all their edges are between adjacent layers. It will take some thoughts and probably a lot of trials and errors to figure out what data structures are most appropriate and what API functions and theorems are needed.