diff --git a/Cslib.lean b/Cslib.lean
index 67b5d493..9cec8a39 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,13 +1,16 @@
+import Cslib.Computability.Automata.Acceptor
 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.DAToNA
+import Cslib.Computability.Automata.EpsilonNA
+import Cslib.Computability.Automata.EpsilonNAToNA
 import Cslib.Computability.Automata.NA
-import Cslib.Computability.Automata.NFA
-import Cslib.Computability.Automata.NFAToDFA
+import Cslib.Computability.Automata.NAToDA
+import Cslib.Computability.Automata.OmegaAcceptor
+import Cslib.Computability.Automata.Prod
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Computability.Languages.OmegaRegularLanguage
+import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Foundations.Control.Monad.Free
 import Cslib.Foundations.Control.Monad.Free.Effects
 import Cslib.Foundations.Control.Monad.Free.Fold
@@ -21,6 +24,9 @@ import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Lint.Basic
 import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.LTS.FLTSToLTS
+import Cslib.Foundations.Semantics.LTS.LTSToFLTS
 import Cslib.Foundations.Semantics.LTS.Simulation
 import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Semantics.ReductionSystem.Basic
diff --git a/Cslib/Computability/Automata/Acceptor.lean b/Cslib/Computability/Automata/Acceptor.lean
new file mode 100644
index 00000000..b323b6d4
--- /dev/null
+++ b/Cslib/Computability/Automata/Acceptor.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Languages.Language
+
+namespace Cslib.Automata
+
+/-- An `Acceptor` is a machine that recognises strings (lists of symbols in an alphabet). -/
+class Acceptor (A : Type _) (Symbol : outParam (Type _)) where
+  /-- Predicate that establishes whether a string `xs` is accepted. -/
+  Accepts (a : A) (xs : List Symbol) : Prop
+
+namespace Acceptor
+
+variable {Symbol : Type _}
+
+/-- The language of an `Acceptor` is the set of strings it `Accepts`. -/
+@[scoped grind .]
+def language [Acceptor A Symbol] (a : A) : Language Symbol :=
+  { xs | Accepts a xs }
+
+/-- A string is in the language of an acceptor iff the acceptor accepts it. -/
+@[scoped grind =]
+theorem mem_language [Acceptor A Symbol] (a : A) (xs : List Symbol) :
+  xs ∈ language a ↔ Accepts a xs := Iff.rfl
+
+end Acceptor
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean
index e7bb94ad..441ab370 100644
--- a/Cslib/Computability/Automata/DA.lean
+++ b/Cslib/Computability/Automata/DA.lean
@@ -1,24 +1,94 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Computability.Automata.Acceptor
+import Cslib.Computability.Automata.OmegaAcceptor
+import Cslib.Computability.Languages.OmegaLanguage
 
+/-! # Deterministic Automata
 
+A Deterministic Automaton (`DA`) is an automaton defined by a transition function equipped with an
+initial state.
 
-/-! # Deterministic Automaton
+Automata with different accepting conditions are then defined as extensions of `DA`.
+These include, for example, a generalised version of DFA as found in the literature (without
+finiteness assumptions), deterministic Buchi automata, and deterministic Muller automata.
 
-A Deterministic Automaton (DA) is an automaton defined by a transition function.
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
-namespace Cslib
+namespace Cslib.Automata
 
-structure DA (State : Type _) (Symbol : Type _) where
+structure DA (State Symbol : Type*) extends FLTS State Symbol where
   /-- The initial state of the automaton. -/
   start : State
-  /-- The transition function of the automaton. -/
-  tr : State → Symbol → State
 
-end Cslib
+namespace DA
+
+variable {State : Type _} {Symbol : Type _}
+
+/-- A deterministic automaton that accepts finite strings (lists of symbols). -/
+structure FinAcc (State Symbol : Type*) extends DA State Symbol where
+  /-- The accept states. -/
+  accept : Set State
+
+namespace FinAcc
+
+/-- A `DA.FinAcc` accepts a string if its multistep transition function maps the start state and
+the string to an accept state.
+
+This is the standard string recognition performed by DFAs in the literature. -/
+@[scoped grind =]
+instance : Acceptor (DA.FinAcc State Symbol) Symbol where
+  Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) := a.mtr a.start xs ∈ a.accept
+
+end FinAcc
+
+/-- Helper function for defining `run` below. -/
+@[simp, scoped grind =]
+def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
+  | 0 => da.start
+  | n + 1 => da.tr (run' da xs n) (xs n)
+
+/-- Infinite run. -/
+@[scoped grind =]
+def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
+
+open List Filter
+
+/-- Deterministic Buchi automaton. -/
+structure Buchi (State Symbol : Type*) extends DA State Symbol where
+  /-- The accept states -/
+  accept : Set State
+
+namespace Buchi
+
+@[scoped grind =]
+instance : ωAcceptor (Buchi State Symbol) Symbol where
+  Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := ∃ᶠ k in atTop, a.run xs k ∈ a.accept
+
+end Buchi
+
+/-- Deterministic Muller automaton. -/
+structure Muller (State Symbol : Type*) extends DA State Symbol where
+  /-- The accepting set of sets of states. -/
+  accept : Set (Set State)
+
+namespace Muller
+
+@[scoped grind =]
+instance : ωAcceptor (Muller State Symbol) Symbol where
+  Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := (a.run xs).infOcc ∈ a.accept
+
+end Muller
+
+end DA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/DAToNA.lean b/Cslib/Computability/Automata/DAToNA.lean
new file mode 100644
index 00000000..128f5f37
--- /dev/null
+++ b/Cslib/Computability/Automata/DAToNA.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Semantics.LTS.FLTSToLTS
+
+/-! # Translation of Deterministic Automata into Nonodeterministic Automata.
+
+This is the general version of the standard translation of DFAs into NFAs. -/
+
+namespace Cslib.Automata.DA
+
+variable {State : Type _} {Symbol : Type _}
+
+section NA
+
+/-- `DA` is a special case of `NA`. -/
+@[scoped grind =]
+def toNA (a : DA State Symbol) : NA State Symbol :=
+  { a.toLTS with start := {a.start} }
+
+instance : Coe (DA State Symbol) (NA State Symbol) where
+  coe := toNA
+
+namespace FinAcc
+
+/-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/
+@[scoped grind =]
+def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol :=
+  { a.toNA with accept := a.accept }
+
+open Acceptor in
+open scoped FLTS NA.FinAcc in
+/-- The `NA` constructed from a `DA` has the same language. -/
+@[scoped grind _=_]
+theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
+    language a.toNAFinAcc = language a := by
+  ext xs
+  constructor
+  · grind
+  · intro _
+    use a.start
+    grind
+
+end FinAcc
+
+end NA
+
+end Cslib.Automata.DA
diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean
deleted file mode 100644
index 88c38b7f..00000000
--- a/Cslib/Computability/Automata/DFA.lean
+++ /dev/null
@@ -1,67 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Computability.Automata.DA
-import Cslib.Computability.Languages.Language
-
-/-! # Deterministic Finite-State Automata
-
-A Deterministic Finite Automaton (DFA) is a finite-state machine that accepts or rejects
-a finite string.
-
-## References
-
-* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
-  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
--/
-
-namespace Cslib
-
-/-- A Deterministic Finite Automaton (DFA) 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 accepting states `accept`. -/
-structure DFA (State : Type _) (Symbol : Type _) extends DA 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 DFA
-
-variable {State : Type _} {Symbol : Type _}
-
-/-- Extended transition function.
-
-Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
-from the left (instead of the right), in order to match the way lists are constructed.
--/
-@[scoped grind =]
-def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s
-
-@[scoped grind =]
-theorem mtr_nil_eq {dfa : DFA State Symbol} {s : State} : dfa.mtr s [] = s := rfl
-
-/-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
-the start state. -/
-@[scoped grind →]
-def Accepts (dfa : DFA State Symbol) (xs : List Symbol) :=
-  dfa.mtr dfa.start xs ∈ dfa.accept
-
-/-- The language of a DFA is the set of strings that it accepts. -/
-@[scoped grind =]
-def language (dfa : DFA State Symbol) : Language Symbol :=
-  { xs | dfa.Accepts xs }
-
-/-- A string is in the language of a DFA iff it is accepted by the DFA. -/
-@[scoped grind =]
-theorem mem_language (dfa : DFA State Symbol) (xs : List Symbol) :
-  xs ∈ dfa.language ↔ dfa.Accepts xs := Iff.rfl
-
-end DFA
-
-end Cslib
diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean
deleted file mode 100644
index 35602e71..00000000
--- a/Cslib/Computability/Automata/DFAToNFA.lean
+++ /dev/null
@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Computability.Automata.DFA
-import Cslib.Computability.Automata.NFA
-
-/-! # Translation of DFA into NFA -/
-
-namespace Cslib
-
-namespace DFA
-
-variable {State : Type _} {Symbol : Type _}
-
-section NFA
-
-/-- `DFA` is a special case of `NFA`. -/
-@[scoped grind =]
-def toNFA (dfa : DFA State Symbol) : NFA State Symbol where
-  start := {dfa.start}
-  accept := dfa.accept
-  Tr := fun s1 μ s2 => dfa.tr s1 μ = s2
-  finite_state := dfa.finite_state
-  finite_symbol := dfa.finite_symbol
-
-@[scoped grind =]
-lemma toNFA_start {dfa : DFA State Symbol} : dfa.toNFA.start = {dfa.start} := rfl
-
-instance : Coe (DFA State Symbol) (NFA State Symbol) where
-  coe := toNFA
-
-/-- `DA.toNA` correctly characterises transitions. -/
-@[scoped grind =]
-theorem toNA_tr {dfa : DFA State Symbol} {s1 s2 : State} {μ : Symbol} :
-  dfa.toNFA.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by
-  rfl
-
-/-- The transition system of a DA is deterministic. -/
-@[scoped grind ⇒]
-theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by
-  grind
-
-/-- The transition system of a DA is image-finite. -/
-@[scoped grind ⇒]
-theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite :=
-  dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic
-
-/-- Characterisation of multistep transitions. -/
-@[scoped grind =]
-theorem toNFA_mtr {dfa : DFA State Symbol} {s1 s2 : State} {xs : List Symbol} :
-  dfa.toNFA.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by
-  have : ∀ x, dfa.toNFA.Tr s1 x (dfa.tr s1 x) := by grind
-  constructor <;> intro h
-  case mp => induction h <;> grind
-  case mpr => induction xs generalizing s1 <;> grind
-
-/-- The `NFA` constructed from a `DFA` has the same language. -/
-@[scoped grind =]
-theorem toNFA_language_eq {dfa : DFA State Symbol} :
-  dfa.toNFA.language = dfa.language := by
-  ext xs
-  refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> open NFA in grind
-
-end NFA
-
-end DFA
-
-end Cslib
diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA.lean
new file mode 100644
index 00000000..f0d6992b
--- /dev/null
+++ b/Cslib/Computability/Automata/EpsilonNA.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.NA
+import Cslib.Computability.Automata.Acceptor
+
+/-! # Nondeterministic automata with ε-transitions. -/
+
+namespace Cslib.Automata
+
+/-- A nondeterministic finite automaton with ε-transitions (`εNA`) is an `NA` with an `Option`
+symbol type. The special symbol ε is represented by the `Option.none` case.
+
+Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
+allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
+ε-closure. -/
+structure εNA (State Symbol : Type*) extends NA State (Option Symbol)
+
+variable {State Symbol : Type*}
+
+@[local grind =]
+private instance : HasTau (Option α) := ⟨.none⟩
+
+/-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S`
+by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance
+of `HasTau.τ`. -/
+abbrev εNA.εClosure (a : εNA State Symbol) (S : Set State) := a.τClosure S
+
+namespace εNA
+
+structure FinAcc (State Symbol : Type*) extends εNA State Symbol where
+  accept : Set State
+
+namespace FinAcc
+
+/-- An `εNA.FinAcc` accepts a string if there is a saturated multistep accepting derivative with
+that trace from the start state. -/
+@[scoped grind =]
+instance : Acceptor (FinAcc State Symbol) Symbol where
+  Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
+    ∃ s ∈ a.εClosure a.start, ∃ s' ∈ a.accept,
+    a.saturate.MTr s (xs.map (some ·)) s'
+
+end FinAcc
+
+end εNA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/EpsilonNAToNA.lean b/Cslib/Computability/Automata/EpsilonNAToNA.lean
new file mode 100644
index 00000000..3941453a
--- /dev/null
+++ b/Cslib/Computability/Automata/EpsilonNAToNA.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.EpsilonNA
+
+/-! # Translation of εNA into NA -/
+
+namespace Cslib
+
+/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
+ε-transitions. -/
+@[local grind =]
+private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
+  Tr s μ s' := lts.Tr s (some μ) s'
+
+@[local grind .]
+private lemma LTS.noε_saturate_tr
+  {lts : LTS State (Option Label)} {h : μ = some μ'} :
+  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
+  simp only [LTS.noε]
+  grind
+
+@[scoped grind =]
+lemma LTS.noε_saturate_mTr {lts : LTS State (Option Label)} :
+  lts.saturate.MTr s (μs.map some) = lts.saturate.noε.MTr s μs := by
+  ext s'
+  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
+
+namespace Automata.εNA.FinAcc
+
+variable {State Symbol : Type*}
+
+/-- Any `εNA.FinAcc` can be converted into an `NA.FinAcc` that does not use ε-transitions. -/
+@[scoped grind]
+def toNAFinAcc (a : εNA.FinAcc State Symbol) : NA.FinAcc State Symbol where
+  start := a.εClosure a.start
+  accept := a.accept
+  Tr := a.saturate.noε.Tr
+
+open Acceptor in
+open scoped NA.FinAcc in
+/-- Correctness of `toNAFinAcc`. -/
+@[scoped grind _=_]
+theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
+    language ena.toNAFinAcc = language ena := by
+  ext xs
+  have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
+    simp [LTS.noε_saturate_mTr]
+  grind
+
+end Automata.εNA.FinAcc
+
+end Cslib
diff --git a/Cslib/Computability/Automata/EpsilonNFA.lean b/Cslib/Computability/Automata/EpsilonNFA.lean
deleted file mode 100644
index 69997dc1..00000000
--- a/Cslib/Computability/Automata/EpsilonNFA.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Computability.Automata.NA
-import Cslib.Computability.Languages.Language
-
-/-! # Nondeterministic automata with ε-transitions. -/
-
-namespace Cslib
-
-/-- A nondeterministic finite automaton with ε-transitions (`εNFA`) is an `NA` with an `Option`
-symbol type. The special symbol ε is represented by the `Option.none` case.
-
-Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
-allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
-ε-closure. -/
-structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option 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
-
-variable {State : Type _} {Symbol : Type _}
-
-@[local grind =]
-private instance : HasTau (Option α) := ⟨.none⟩
-
-/-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S`
-by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance
-of `HasTau.τ`. -/
-abbrev εNFA.εClosure (enfa : εNFA State Symbol) (S : Set State) := enfa.τClosure S
-
-namespace εNFA
-
-/-- An εNFA accepts a string if there is a saturated multistep accepting derivative with that trace
-from the start state. -/
-@[scoped grind]
-def Accepts (enfa : εNFA State Symbol) (xs : List Symbol) :=
-  ∃ s ∈ enfa.εClosure enfa.start, ∃ s' ∈ enfa.accept,
-  enfa.saturate.MTr s (xs.map (some ·)) s'
-
-/-- The language of an εDA is the set of strings that it accepts. -/
-@[scoped grind =]
-def language (enfa : εNFA State Symbol) : Language Symbol :=
-  { xs | enfa.Accepts xs }
-
-/-- A string is in the language of an εNFA iff it is accepted by the εNFA. -/
-@[scoped grind =]
-theorem mem_language (enfa : εNFA State Symbol) (xs : List Symbol) :
-  xs ∈ enfa.language ↔ enfa.Accepts xs := by rfl
-
-end εNFA
-
-end Cslib
diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
deleted file mode 100644
index 445e14f4..00000000
--- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
+++ /dev/null
@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Computability.Automata.EpsilonNFA
-import Cslib.Computability.Automata.NFA
-
-/-! # Translation of εNFA into NFA -/
-
-namespace Cslib
-
-open Cslib
-/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
-ε-transitions. -/
-@[grind]
-private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
-  Tr := fun s μ s' => lts.Tr s (some μ) s'
-
-@[local grind .]
-private lemma LTS.noε_saturate_tr
-  {lts : LTS State (Option Label)} {h : μ = some μ'} :
-  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
-  simp only [LTS.noε]
-  grind
-
-namespace εNFA
-
-variable {State : Type _} {Symbol : Type _}
-
-section NFA
-
-/-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/
-@[scoped grind]
-def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
-  start := enfa.εClosure enfa.start
-  accept := enfa.accept
-  Tr := enfa.saturate.noε.Tr
-  finite_state := enfa.finite_state
-  finite_symbol := enfa.finite_symbol
-
-@[scoped grind =]
-lemma LTS.noε_saturate_mTr {s : State} {Label : Type _} {μs : List Label}
-  {lts : LTS State (Option Label)} :
-  lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
-  ext s'
-  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
-
-
-/-- Correctness of `toNFA`. -/
-@[scoped grind =]
-theorem toNFA_language_eq {enfa : εNFA State Symbol} :
-  enfa.toNFA.language = enfa.language := by
-  ext xs
-  have : ∀ s s', enfa.saturate.MTr s (xs.map (some ·)) s' = enfa.saturate.noε.MTr s xs s' := by
-    simp [LTS.noε_saturate_mTr]
-  open NFA in grind
-
-end NFA
-end εNFA
-
-end Cslib
diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean
index 0c119cc1..6c6fbfa5 100644
--- a/Cslib/Computability/Automata/NA.lean
+++ b/Cslib/Computability/Automata/NA.lean
@@ -1,24 +1,94 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
+import Cslib.Computability.Languages.OmegaLanguage
 import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Computability.Automata.Acceptor
+import Cslib.Computability.Automata.OmegaAcceptor
 
 /-! # Nondeterministic Automaton
 
-A Nondeterministic Automaton (NA) is an automaton with a set of initial states.
+A Nondeterministic Automaton (NA) is a transition relation equipped with a set of initial states.
+
+Automata with different accepting conditions are then defined as extensions of `NA`.
+These include, for example, a generalised version of NFA as found in the literature (without
+finiteness assumptions), nondeterministic Buchi automata, and nondeterministic Muller automata.
 
 This definition extends `LTS` and thus stores the transition system as a relation `Tr` of the form
 `State → Symbol → State → Prop`. Note that you can also instantiate `Tr` by passing an argument of
 type `State → Symbol → Set State`; it gets automatically expanded to the former shape.
+
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
-namespace Cslib
+open Filter
 
-structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
+namespace Cslib.Automata
+
+structure NA (State Symbol : Type*) extends LTS State Symbol where
   /-- The set of initial states of the automaton. -/
   start : Set State
 
-end Cslib
+namespace NA
+
+variable {State : Type _} {Symbol : Type _}
+
+/-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/
+structure FinAcc (State Symbol : Type*) extends NA State Symbol where
+  /-- The accept states. -/
+  accept : Set State
+
+namespace FinAcc
+
+/-- An `NA.FinAcc` accepts a string if there is a multistep transition from a start state to an
+accept state.
+
+This is the standard string recognition performed by NFAs in the literature. -/
+@[scoped grind =]
+instance : Acceptor (FinAcc State Symbol) Symbol where
+  Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
+    ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s'
+
+end FinAcc
+
+/-- Infinite run. -/
+@[scoped grind =]
+def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) :=
+  ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))
+
+/-- Nondeterministic Buchi automaton. -/
+structure Buchi (State Symbol : Type*) extends NA State Symbol where
+  accept : Set State
+
+namespace Buchi
+
+@[scoped grind =]
+instance : ωAcceptor (Buchi State Symbol) Symbol where
+  Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
+    ∃ ss, ∃ᶠ k in atTop, a.Run xs ss ∧ ss k ∈ a.accept
+
+end Buchi
+
+/-- Nondeterministic Muller automaton. -/
+structure Muller (State Symbol : Type*) extends NA State Symbol where
+  accept : Set (Set State)
+
+namespace Muller
+
+@[scoped grind =]
+instance : ωAcceptor (Muller State Symbol) Symbol where
+  Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
+    ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept
+
+end Muller
+
+end NA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/NAToDA.lean b/Cslib/Computability/Automata/NAToDA.lean
new file mode 100644
index 00000000..af327ab1
--- /dev/null
+++ b/Cslib/Computability/Automata/NAToDA.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Semantics.LTS.LTSToFLTS
+
+/-! # Translation of Nondeterministic Automata for finite strings into Deterministic Automata
+
+This file implements the standard subset construction.
+-/
+
+namespace Cslib.Automata.NA
+
+variable {State : Type _} {Symbol : Type _}
+
+section SubsetConstruction
+
+/-- Converts an `NA` into a `DA` using the subset construction. -/
+@[scoped grind =]
+def toDA (a : NA State Symbol) : DA (Set State) Symbol :=
+  { a.toFLTS with start := a.start }
+
+namespace FinAcc
+
+/-- Converts an `NA.FinAcc` into a `DA.FinAcc` using the subset construction. -/
+@[scoped grind =]
+def toDAFinAcc (a : NA.FinAcc State Symbol) : DA.FinAcc (Set State) Symbol :=
+  { a.toDA with accept := { S | ∃ s ∈ S, s ∈ a.accept } }
+
+open Acceptor in
+open scoped DA.FinAcc LTS in
+/-- The `DA` constructed from an `NA` has the same language. -/
+@[scoped grind _=_]
+theorem toDAFinAcc_language_eq {na : NA.FinAcc State Symbol} :
+  language na.toDAFinAcc = language na := by
+  ext xs
+  #adaptation_note
+  /--
+  Moving from `nightly-2025-09-15` to `nightly-2025-10-19` required
+  increasing the number of allowed splits.
+  -/
+  grind (splits := 11)
+
+end FinAcc
+
+end SubsetConstruction
+
+end Cslib.Automata.NA
diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean
deleted file mode 100644
index a83b9efb..00000000
--- a/Cslib/Computability/Automata/NFA.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Computability.Automata.NA
-import Cslib.Computability.Languages.Language
-
-namespace Cslib
-
-/-- A Nondeterministic Finite Automaton (NFA) is a nondeterministic automaton (NA)
-over finite sets of states and symbols. -/
-structure NFA (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 NFA
-
-variable {State : Type _} {Symbol : Type _}
-
-/-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
-the start state. -/
-@[scoped grind]
-def Accepts (nfa : NFA State Symbol) (xs : List Symbol) :=
-  ∃ s ∈ nfa.start, ∃ s' ∈ nfa.accept, nfa.MTr s xs s'
-
-/-- The language of an NFA is the set of strings that it accepts. -/
-@[scoped grind]
-def language (nfa : NFA State Symbol) : Language Symbol :=
-  { xs | nfa.Accepts xs }
-
-/-- A string is in the language of an NFA iff it is accepted by the NFA. -/
-@[scoped grind =]
-theorem mem_language (nfa : NFA State Symbol) (xs : List Symbol) :
-  xs ∈ nfa.language ↔ nfa.Accepts xs := Iff.rfl
-
-end NFA
-
-end Cslib
diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean
deleted file mode 100644
index 1536b662..00000000
--- a/Cslib/Computability/Automata/NFAToDFA.lean
+++ /dev/null
@@ -1,75 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Computability.Automata.DFA
-import Cslib.Computability.Automata.NFA
-
-/-! # Translation of NFA into DFA (subset construction) -/
-
-namespace Cslib
-
-namespace NFA
-
-variable {State : Type _} {Symbol : Type _}
-
-section SubsetConstruction
-
-/-- Converts an `NFA` into a `DFA` using the subset construction. -/
-@[scoped grind =]
-def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := {
-  start := nfa.start
-  accept := { S | ∃ s ∈ S, s ∈ nfa.accept }
-  tr := nfa.setImage
-  finite_state := by
-    haveI := nfa.finite_state
-    infer_instance
-  finite_symbol := nfa.finite_symbol
-}
-
-/-- Characterisation of transitions in `NFA.toDFA` wrt transitions in the original NA. -/
-@[scoped grind =]
-theorem toDFA_mem_tr {nfa : NFA State Symbol} {S : Set State} {s' : State} {x : Symbol} :
-  s' ∈ nfa.toDFA.tr S x ↔ ∃ s ∈ S, nfa.Tr s x s' := by
-  simp only [NFA.toDFA, LTS.setImage, Set.mem_iUnion, exists_prop]
-  grind
-
-/-- Characterisation of multistep transitions in `NFA.toDFA` wrt multistep transitions in the
-original NA. -/
-@[scoped grind =]
-theorem toDFA_mem_mtr {nfa : NFA State Symbol} {S : Set State} {s' : State} {xs : List Symbol} :
-  s' ∈ nfa.toDFA.mtr S xs ↔ ∃ s ∈ S, nfa.MTr s xs s' := by
-  simp only [NFA.toDFA, DFA.mtr]
-  /- TODO: Grind does not catch a useful rewrite in the subset construction for automata
-
-    A very similar issue seems to occur in the proof of `NFA.toDFA_language_eq`.
-
-    labels: grind, lts, automata
-  -/
-  rw [← LTS.setImageMultistep_foldl_setImage]
-  grind
-
-/-- Characterisation of multistep transitions in `NFA.toDFA` as image transitions in `LTS`. -/
-@[scoped grind =]
-theorem toDFA_mtr_setImageMultistep {nfa : NFA State Symbol} :
-  nfa.toDFA.mtr = nfa.setImageMultistep := by grind
-
-/-- The `DFA` constructed from an `NFA` has the same language. -/
-@[scoped grind =]
-theorem toDFA_language_eq {nfa : NFA State Symbol} :
-  nfa.toDFA.language = nfa.language := by
-  ext xs
-  rw [DFA.mem_language]
-  #adaptation_note
-  /--
-  Moving from `nightly-2025-09-15` to `nightly-2025-10-19` required
-  increasing the number of allowed splits.
-  -/
-  open DFA in grind (splits := 11)
-
-end SubsetConstruction
-end NFA
-
-end Cslib
diff --git a/Cslib/Computability/Automata/OmegaAcceptor.lean b/Cslib/Computability/Automata/OmegaAcceptor.lean
new file mode 100644
index 00000000..3b423f81
--- /dev/null
+++ b/Cslib/Computability/Automata/OmegaAcceptor.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Languages.OmegaLanguage
+
+namespace Cslib.Automata
+
+/-- An `ωAcceptor` is a machine that recognises infinite sequences of symbols. -/
+class ωAcceptor (A : Type _) (Symbol : outParam (Type _)) where
+  /-- Predicate that establishes whether a string `xs` is accepted. -/
+  Accepts (a : A) (xs : ωSequence Symbol) : Prop
+
+namespace ωAcceptor
+
+variable {Symbol : Type _}
+
+/-- The language of an `ωAcceptor` is the set of sequences it `Accepts`. -/
+@[scoped grind .]
+def language [ωAcceptor A Symbol] (a : A) : ωLanguage Symbol :=
+  { xs | Accepts a xs }
+
+/-- A string is in the language of an acceptor iff the acceptor accepts it. -/
+@[scoped grind =]
+theorem mem_language [ωAcceptor A Symbol] (a : A) (xs : ωSequence Symbol) :
+  xs ∈ language a ↔ Accepts a xs := Iff.rfl
+
+end ωAcceptor
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/Prod.lean b/Cslib/Computability/Automata/Prod.lean
new file mode 100644
index 00000000..0d39c758
--- /dev/null
+++ b/Cslib/Computability/Automata/Prod.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.DA
+
+/-! # Product of automata. -/
+
+namespace Cslib.Automata
+
+open List
+open scoped FLTS
+
+variable {State1 State2 Symbol : Type*}
+
+namespace DA
+
+/-
+TODO: This operation could be generalised to FLTS and lifted here.
+-/
+@[scoped grind =]
+def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
+  start := (da1.start, da2.start)
+  tr := fun (s1, s2) x ↦ (da1.tr s1 x, da2.tr s2 x)
+
+@[simp, scoped grind =]
+theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
+    (s : State1 × State2) (xs : List Symbol) :
+    (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) := by
+  induction xs generalizing s <;> grind
+
+end DA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean
index 1cd97437..da1e95cf 100644
--- a/Cslib/Computability/Languages/Language.lean
+++ b/Cslib/Computability/Languages/Language.lean
@@ -20,7 +20,25 @@ namespace Language
 open Set List
 open scoped Computability
 
-variable {α : Type _} {l : Language α}
+variable {α : Type*} {l m : Language α}
+
+@[simp, scoped grind =]
+theorem mem_inf (x : List α) : x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m :=
+  Iff.rfl
+
+@[simp]
+theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
+    (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i :=
+  mem_iInter₂
+
+@[simp]
+theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
+    (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i := by
+  constructor <;> intro h
+  · have := mem_iUnion₂.mp h
+    grind
+  · apply mem_iUnion₂.mpr
+    grind
 
 -- This section will be removed once the following PR gets into mathlib:
 -- https://github.com/leanprover-community/mathlib4/pull/30913
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index cb6d0239..dc646fd7 100644
--- a/Cslib/Computability/Languages/OmegaLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -59,7 +59,7 @@ open scoped Computability
 
 universe v
 
-variable {α β γ : Type _}
+variable {α β γ : Type*}
 
 /-- An ω-language is a set of strings over an alphabet. -/
 def ωLanguage (α) :=
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
new file mode 100644
index 00000000..58493c3f
--- /dev/null
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 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 Cslib.Computability.Automata.NA
+import Mathlib.Tactic
+
+/-!
+# ω-Regular languages
+
+This file defines ω-regular languages and proves some properties of them.
+-/
+
+open Set Function
+open scoped Computability
+open Cslib.Automata
+
+namespace Cslib.ωLanguage
+
+variable {Symbol : Type*}
+
+/-- An ω-regular language is one that is accepted by a finite-state Buchi automaton. -/
+def IsRegular (p : ωLanguage Symbol) :=
+  ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, ωAcceptor.language na = p
+
+/-- There is an ω-regular language which is not accepted by any deterministic Buchi automaton. -/
+proof_wanted IsRegular.not_det_buchi :
+  ∃ p : ωLanguage Symbol, p.IsRegular ∧
+    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, ωAcceptor.language da = p
+
+/-- McNaughton's Theorem. -/
+proof_wanted IsRegular.iff_muller_lang {p : ωLanguage Symbol} :
+    p.IsRegular ↔
+    ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, ωAcceptor.language da = p
+
+end Cslib.ωLanguage
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
new file mode 100644
index 00000000..454a7664
--- /dev/null
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2025 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.DAToNA
+import Cslib.Computability.Automata.NAToDA
+import Cslib.Computability.Automata.Prod
+import Cslib.Computability.Automata.Acceptor
+import Mathlib.Computability.DFA
+import Mathlib.Tactic
+
+/-!
+# Regular languages
+-/
+
+open Set Function List Prod
+open scoped Computability Cslib.FLTS Cslib.Automata.DA Cslib.Automata.NA Cslib.Automata.Acceptor
+  Cslib.Automata.DA.FinAcc Cslib.Automata.NA.FinAcc
+
+namespace Language
+
+variable {Symbol : Type*}
+
+open Cslib.Automata Acceptor in
+/-- A characterization of Language.IsRegular using Cslib.DA -/
+theorem IsRegular.iff_cslib_dfa {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
+      ∃ dfa : DA.FinAcc State Symbol, language dfa = l := by
+  constructor
+  · rintro ⟨State, h_fin, ⟨tr, start, acc⟩, rfl⟩
+    let dfa := DA.FinAcc.mk {tr, start} acc
+    use State, Fintype.finite h_fin, dfa
+    rfl
+  · rintro ⟨State, h_fin, ⟨⟨flts, start⟩, acc⟩, rfl⟩
+    let dfa := DFA.mk flts.tr start acc
+    use State, Fintype.ofFinite State, dfa
+    rfl
+
+open Cslib.Automata Acceptor in
+/-- A characterization of Language.IsRegular using Cslib.NA -/
+theorem IsRegular.iff_cslib_nfa {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
+      ∃ nfa : NA.FinAcc State Symbol, language nfa = l := by
+  rw [IsRegular.iff_cslib_dfa]; constructor
+  · rintro ⟨State, h_fin, ⟨da, acc⟩, rfl⟩
+    use State, h_fin, ⟨da.toNA, acc⟩
+    grind
+  · rintro ⟨State, _, na, rfl⟩
+    use Set State, inferInstance, na.toDAFinAcc
+    grind
+
+-- From this point onward we will use only automata from Cslib in the proofs.
+open Cslib
+
+@[simp]
+theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa] at h ⊢
+  obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := h
+  use State, inferInstance, ⟨da, accᶜ⟩
+  ext; grind
+
+@[simp]
+theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa]
+  let flts := FLTS.mk (fun () (_ : Symbol) ↦ ())
+  use Unit, inferInstance, ⟨Cslib.Automata.DA.mk flts (), ∅⟩
+  grind
+
+@[simp]
+theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa]
+  let flts := FLTS.mk (fun (_ : Fin 2) (_ : Symbol) ↦ 1)
+  use Fin 2, inferInstance, ⟨Cslib.Automata.DA.mk flts 0, {0}⟩
+  ext; constructor
+  · intro h; by_contra h'
+    have := dropLast_append_getLast h'
+    grind
+  · grind [Language.mem_one]
+
+@[simp]
+theorem IsRegular.top : (⊤ : Language Symbol).IsRegular := by
+  have : (⊥ᶜ : Language Symbol).IsRegular := IsRegular.compl <| IsRegular.zero
+  rwa [← compl_bot]
+
+@[simp]
+theorem IsRegular.inf {l1 l2 : Language Symbol}
+    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 ⊓ l2).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa] at h1 h2 ⊢
+  obtain ⟨State1, h_fin1, ⟨da1, acc1⟩, rfl⟩ := h1
+  obtain ⟨State2, h_fin1, ⟨da2, acc2⟩, rfl⟩ := h2
+  use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∩ snd ⁻¹' acc2⟩
+  ext; grind
+
+@[simp]
+theorem IsRegular.add {l1 l2 : Language Symbol}
+    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 + l2).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa] at h1 h2 ⊢
+  obtain ⟨State1, h_fin1, ⟨da1, acc1⟩, rfl⟩ := h1
+  obtain ⟨State2, h_fin1, ⟨da2, acc2⟩, rfl⟩ := h2
+  use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∪ snd ⁻¹' acc2⟩
+  ext; grind [Language.mem_add]
+
+@[simp]
+theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
+    (h : ∀ i ∈ s, (l i).IsRegular) : (⨅ i ∈ s, l i).IsRegular := by
+  generalize h_n : s.ncard = n
+  induction n generalizing s
+  case zero => simp_all [ncard_eq_zero (s := s)]
+  case succ n h_ind =>
+    obtain ⟨i, t, h_i, rfl, rfl⟩ := (ncard_eq_succ (s := s)).mp h_n
+    rw [iInf_insert]
+    grind [IsRegular.inf]
+
+@[simp]
+theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
+    (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular := by
+  generalize h_n : s.ncard = n
+  induction n generalizing s
+  case zero =>
+    obtain ⟨rfl⟩ := (ncard_eq_zero (s := s)).mp h_n
+    simp only [mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot]
+    exact IsRegular.zero
+  case succ n h_ind =>
+    obtain ⟨i, t, h_i, rfl, rfl⟩ := (ncard_eq_succ (s := s)).mp h_n
+    rw [iSup_insert]
+    apply IsRegular.add <;> grind
+
+end Language
diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean
index c3e680f8..7cc81730 100644
--- a/Cslib/Foundations/Data/OmegaSequence/Defs.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/Defs.lean
@@ -7,6 +7,7 @@ import Cslib.Init
 import Mathlib.Data.Nat.Notation
 import Mathlib.Data.FunLike.Basic
 import Mathlib.Logic.Function.Iterate
+import Mathlib.Order.Filter.AtTopBot.Defs
 
 /-!
 # Definition of `ωSequence` and functions on infinite sequences
@@ -23,6 +24,8 @@ Most code below is adapted from Mathlib.Data.Stream.Defs.
 
 namespace Cslib
 
+open Filter
+
 universe u v w
 variable {α : Type u} {β : Type v} {δ : Type w}
 
@@ -85,6 +88,10 @@ def zip (f : α → β → δ) (s₁ : ωSequence α) (s₂ : ωSequence β) : 
 /-- Iterates of a function as an ω-sequence. -/
 def iterate (f : α → α) (a : α) : ωSequence α := fun n => f^[n] a
 
+/-- The set of elements that appear infinitely often in an ω-sequence. -/
+def infOcc (xs : ωSequence α) : Set α :=
+  { x | ∃ᶠ k in atTop, xs k = x }
+
 end ωSequence
 
 end Cslib
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index c8edb4d9..6ea94091 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -56,8 +56,8 @@ namespace Cslib
 universe u v
 
 /--
-A Labelled Transition System (LTS) consists of a type of states (`State`), a type of transition
-labels (`Label`), and a labelled transition relation (`Tr`).
+A Labelled Transition System (LTS) for a type of states (`State`) and a type of transition
+labels (`Label`) consists of a labelled transition relation (`Tr`).
 -/
 structure LTS (State : Type u) (Label : Type v) where
   /-- The transition relation. -/
@@ -405,10 +405,8 @@ def LTS.Acyclic : Prop :=
 def LTS.Finite : Prop :=
   lts.FiniteState ∧ lts.Acyclic
 
-/-
-/-- An LTS has a complete transition relation if every state has a `μ`-derivative for every `μ`. -/
-def LTS.CompleteTr (lts : LTS State Label) : Prop := ∀ s μ, ∃ s', lts.Tr s μ s'
--/
+/-- An LTS is left-total if every state has a `μ`-derivative for every label `μ`. -/
+def LTS.LeftTotal (lts : LTS State Label) : Prop := ∀ s μ, ∃ s', lts.Tr s μ s'
 
 end Classes
 
diff --git a/Cslib/Foundations/Semantics/LTS/FLTS.lean b/Cslib/Foundations/Semantics/LTS/FLTS.lean
new file mode 100644
index 00000000..47bba1a7
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/FLTS.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Init
+
+/-! # Functional Labelled Transition System (FLTS)
+
+A Functional Labelled Transition System is a special case of an `LTS` where transitions are
+determined by a function.
+
+This is a generalisation of deterministic finite-state machines.
+
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
+-/
+
+namespace Cslib
+
+/--
+A Functional Labelled Transition System (`FLTS`) for a type of states (`State`) and a type of
+transition labels (`Label`) consists of a labelled transition function (`tr`).
+-/
+structure FLTS (State : Type _) (Label : Type _) where
+  /-- The transition function. -/
+  tr : State → Label → State
+
+namespace FLTS
+
+variable {State : Type _} {Label : Type _}
+
+/-- Extended transition function.
+
+Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
+from the left (instead of the right), in order to match the way lists are constructed.
+-/
+@[scoped grind =]
+def mtr (flts : FLTS State Label) (s : State) (μs : List Label) := μs.foldl flts.tr s
+
+@[scoped grind =]
+theorem mtr_nil_eq {flts : FLTS State Label} {s : State} : flts.mtr s [] = s := rfl
+
+end FLTS
+
+end Cslib
diff --git a/Cslib/Foundations/Semantics/LTS/FLTSToLTS.lean b/Cslib/Foundations/Semantics/LTS/FLTSToLTS.lean
new file mode 100644
index 00000000..7c607cbf
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/FLTSToLTS.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.LTS.Basic
+
+variable {State : Type _} {Label : Type _}
+
+namespace Cslib.FLTS
+
+/-- `FLTS` is a special case of `LTS`. -/
+@[scoped grind =]
+def toLTS (flts : FLTS State Label) : LTS State Label where
+  Tr s1 μ s2 := flts.tr s1 μ = s2
+
+instance : Coe (FLTS State Label) (LTS State Label) where
+  coe := toLTS
+
+/-- `FLTS.toLTS` correctly characterises transitions. -/
+@[scoped grind =]
+theorem toLTS_tr {flts : FLTS State Label} {s1 : State} {μ : Label} {s2 : State} :
+  flts.toLTS.Tr s1 μ s2 ↔ flts.tr s1 μ = s2 := by rfl
+
+/-- The transition system of a FLTS is deterministic. -/
+@[scoped grind ⇒]
+theorem toLTS_deterministic (flts : FLTS State Label) : flts.toLTS.Deterministic := by
+  grind
+
+/-- The transition system of a FLTS is image-finite. -/
+@[scoped grind ⇒]
+theorem toLTS_imageFinite (flts : FLTS State Label) : flts.toLTS.ImageFinite :=
+  flts.toLTS.deterministic_imageFinite flts.toLTS_deterministic
+
+/-- Characterisation of multistep transitions. -/
+@[scoped grind =]
+theorem toLTS_mtr {flts : FLTS State Label} {s1 : State} {μs : List Label} {s2 : State} :
+    flts.toLTS.MTr s1 μs s2 ↔ flts.mtr s1 μs = s2 := by
+  have : ∀ μ, flts.toLTS.Tr s1 μ (flts.tr s1 μ) := by grind
+  constructor <;> intro h
+  case mp => induction h <;> grind
+  case mpr => induction μs generalizing s1 <;> grind
+
+end Cslib.FLTS
diff --git a/Cslib/Foundations/Semantics/LTS/LTSToFLTS.lean b/Cslib/Foundations/Semantics/LTS/LTSToFLTS.lean
new file mode 100644
index 00000000..5ade2dcb
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/LTSToFLTS.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Semantics.LTS.FLTS
+import Cslib.Foundations.Semantics.LTS.Basic
+
+variable {State : Type _} {Label : Type _}
+
+namespace Cslib.LTS
+
+/-- Converts an `LTS` into an `FLTS` using the subset construction. -/
+@[scoped grind =]
+def toFLTS (lts : LTS State Label) : FLTS (Set State) Label where
+  tr := lts.setImage
+
+/-- Characterisation of transitions in `LTS.toFLTS` wrt transitions in the original `LTS`. -/
+@[scoped grind =]
+theorem toFLTS_mem_tr {lts : LTS State Label} {S : Set State} {s' : State} {μ : Label} :
+  s' ∈ lts.toFLTS.tr S μ ↔ ∃ s ∈ S, lts.Tr s μ s' := by
+  simp only [LTS.toFLTS, LTS.setImage, Set.mem_iUnion, exists_prop]
+  grind
+
+/-- Characterisation of multistep transitions in `LTS.toFLTS` wrt multistep transitions in the
+original `LTS`. -/
+@[scoped grind =]
+theorem toFLTS_mem_mtr {lts : LTS State Label} {S : Set State} {s' : State} {μs : List Label} :
+  s' ∈ lts.toFLTS.mtr S μs ↔ ∃ s ∈ S, lts.MTr s μs s' := by
+  simp only [LTS.toFLTS, FLTS.mtr]
+  /- TODO: Grind does not catch a useful rewrite in the subset construction for automata
+
+    A very similar issue seems to occur in the proof of `LTS.toFLTS_language_eq`.
+
+    labels: grind, lts, automata
+  -/
+  rw [← LTS.setImageMultistep_foldl_setImage]
+  grind
+
+/-- Characterisation of multistep transitions in `LTS.toFLTS` as image transitions in `LTS`. -/
+@[scoped grind =]
+theorem toFLTS_mtr_setImageMultistep {lts : LTS State Label} :
+  lts.toFLTS.mtr = lts.setImageMultistep := by grind
+
+end Cslib.LTS
diff --git a/CslibTests/DFA.lean b/CslibTests/DFA.lean
index a9cb097e..e0159fcd 100644
--- a/CslibTests/DFA.lean
+++ b/CslibTests/DFA.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.Automata.DFA
+import Cslib.Computability.Automata.DA
 
 namespace CslibTests
 
-open Cslib
+open Cslib.Automata
 
 /-! A simple elevator. -/
 
@@ -43,12 +43,9 @@ def tr (floor : Floor) (dir : Direction) : Floor :=
   | .two, .up => .two
   | .two, .down => .one
 
-def elevator : Cslib.DFA Floor Direction := {
+def elevator : DA Floor Direction := {
   tr := tr
   start := .one
-  accept := { Floor.one }
-  finite_state := Floor.finite
-  finite_symbol := Direction.finite
 }
 
 end CslibTests