feat: An initial version of Buchi and Muller automata

Author: ctchou

Cslib.lean

@@ -1,8 +1,10 @@
+import Cslib.Computability.Automata.BuchiNA
 import Cslib.Computability.Automata.DA
 import Cslib.Computability.Automata.DFA
 import Cslib.Computability.Automata.DFAToNFA
 import Cslib.Computability.Automata.EpsilonNFA
 import Cslib.Computability.Automata.EpsilonNFAToNFA
+import Cslib.Computability.Automata.MullerDA
 import Cslib.Computability.Automata.NA
 import Cslib.Computability.Automata.NFA
 import Cslib.Computability.Automata.NFAToDFA

Cslib/Computability/Automata/BuchiNA.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025-present Ching-Tsun Chou All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.NA
+import Mathlib.Order.Filter.AtTopBot.Defs
+
+open Filter
+
+/-- Nondeterministic Büchi automaton is a nondeterministic automaton over
+finite sets of states and symbols together with a finite set of accepting states. -/
+structure BuchiNA (State : Type _) (Symbol : Type _) extends NA State Symbol where
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
+  /-- The automaton is finite-state. -/
+  finite_state : Finite State
+  /-- The type of symbols (also called 'alphabet') is finite. -/
+  finite_symbol : Finite Symbol
+
+namespace BuchiNA
+
+variable {State : Type _} {Symbol : Type _}
+
+/-- A nondeterministic Büchi automaton accepts an ω-word `xs` iff it has an infinite run
+on `xs` which passes through accepting states infinitely often.
+-/
+@[scoped grind]
+def Accepts (nba : BuchiNA State Symbol) (xs : ωList Symbol) :=
+  ∃ ss, nba.InfRun xs ss ∧ ∃ᶠ k in atTop, ss k ∈ nba.accept
+
+/-- The language of a nondeterministic Büchi automaton is the set of ω-words that it accepts. -/
+@[scoped grind]
+def language (nba : BuchiNA State Symbol) : Set (ωList Symbol) :=
+  { xs | nba.Accepts xs }
+
+/-- A string is accepted by a a nondeterministic Büchi automaton iff it is in its language. -/
+@[scoped grind]
+theorem accepts_mem_language (nba : BuchiNA State Symbol) (xs : ωList Symbol) :
+  nba.Accepts xs ↔ xs ∈ nba.language := by rfl
+
+end BuchiNA

Cslib/Computability/Automata/DA.lean

@@ -5,6 +5,7 @@ Authors: Fabrizio Montesi
 -/
 
 import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Data.OmegaList.Init
 
 /-! # Deterministic Automaton
 
@@ -15,3 +16,11 @@ structure DA (State : Type _) (Symbol : Type _) where
   start : State
   /-- The transition function of the automaton. -/
   tr : State → Symbol → State
+
+variable {State : Type _} {Symbol : Type _}
+
+/-- The (unique) infinite run of a DA on an infinite input `xs`.
+-/
+def DA.infRun (da : DA State Symbol) (xs : ωList Symbol) : ωList State
+  | 0 => da.start
+  | k + 1 => da.tr (da.infRun xs k) (xs k)

Cslib/Computability/Automata/MullerDA.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025-present Ching-Tsun Chou All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.DA
+import Mathlib.Order.Filter.AtTopBot.Defs
+
+open Filter
+
+/-! # Deterministic Muller Automata
+-/
+
+/-- `xs.infOcc` is the set of elements that occurs infinitely many times in `xs`.
+TODO: This definition should be be moved to a different file.
+-/
+def ωList.infOcc {X : Type*} (xs : ωList X) : Set X :=
+  { x | ∃ᶠ k in atTop, xs k = x }
+
+/-- A deterministic Muller automaton consists of a labelled transition function
+`tr` over finite sets of states and labels (called symbols), a starting state `start`,
+and a finite set of finite accepting sets `accept`. -/
+structure MullerDA (State : Type _) (Symbol : Type _) extends DA State Symbol where
+  /-- The set of accepting sets of the automaton. -/
+  accept : Set (Set State)
+  /-- The automaton is finite-state. -/
+  finite_state : Finite State
+  /-- The type of symbols (also called 'alphabet') is finite. -/
+  finite_symbol : Finite Symbol
+
+namespace MullerDA
+
+variable {State : Type _} {Symbol : Type _}
+
+/-- A deterministic Muller automaton `mda` accepts an ω-word `xs` iff the set of states that
+occurs infinite often when running `mda` on `xs` is one of the accepting sets.
+-/
+@[scoped grind →]
+def Accepts (mda : MullerDA State Symbol) (xs : ωList Symbol) :=
+  (mda.infRun xs).infOcc ∈ mda.accept
+
+/-- The ω-language of a deterministic Muller automaton is the set of ω-words that it accepts. -/
+@[scoped grind =]
+def language (mda : MullerDA State Symbol) : Set (ωList Symbol) :=
+  { xs | mda.Accepts xs }
+
+/-- An ω-word is accepted by a deterministic Muller automaton iff it is in its ω-language. -/
+@[scoped grind _=_]
+theorem accepts_mem_language (mda : MullerDA State Symbol) (xs : ωList Symbol) :
+  mda.Accepts xs ↔ xs ∈ mda.language := by rfl
+
+end MullerDA

Cslib/Computability/Automata/NA.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+import Cslib.Foundations.Data.OmegaList.Init
 import Cslib.Foundations.Semantics.LTS.Basic
 
 /-! # Nondeterministic Automaton
@@ -17,3 +18,8 @@ type `State → Symbol → Set State`; it gets automatically expanded to the for
 structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
   /-- The set of initial states of the automaton. -/
   start : Set State
+
+variable {State : Type _} {Symbol : Type _}
+
+def NA.InfRun (na : NA State Symbol) (xs : ωList Symbol) (ss : ωList State) :=
+  ss 0 ∈ na.start ∧ ∀ k, na.Tr (ss k) (xs k) (ss (k + 1))