Deterministic Automata

A Deterministic Automaton (DA) is an automaton defined by a transition function equipped with an initial state.

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.

References

• [J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation][Hopcroft2006]

structure Cslib.Automata.DA (State : Type u_1) (Symbol : Type u_2) extends Cslib.FLTS State Symbol : Type (max u_1 u_2)

A deterministic automaton extends a FLTS with a unique initial state.

• tr : State → Symbol → State
• start : State

  The initial state of the automaton.

def Cslib.Automata.DA.run' {State : Type u_1} {Symbol : Type u_2} (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State

Helper function for defining run below.

Equations

• da.run' xs 0 = da.start
• da.run' xs n.succ = da.tr (da.run' xs n) (xs n)

def Cslib.Automata.DA.run {State : Type u_1} {Symbol : Type u_2} (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State

Infinite run.

Equations

• da.run xs = { get := da.run' xs }

@[simp]

theorem Cslib.Automata.DA.run_zero {State : Type u_1} {Symbol : Type u_2} {da : DA State Symbol} {xs : ωSequence Symbol} : (da.run xs) 0 = da.start

@[simp]

theorem Cslib.Automata.DA.run_succ {State : Type u_1} {Symbol : Type u_2} {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} : (da.run xs) (n + 1) = da.tr ((da.run xs) n) (xs n)

@[simp]

theorem Cslib.Automata.DA.mtr_extract_eq_run {State : Type u_1} {Symbol : Type u_2} {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} : da.mtr da.start (xs.extract 0 n) = (da.run xs) n

structure Cslib.Automata.DA.FinAcc (State : Type u_3) (Symbol : Type u_4) extends Cslib.Automata.DA State Symbol : Type (max u_3 u_4)

A deterministic automaton that accepts finite strings (lists of symbols).

• tr : State → Symbol → State
• start : State
• accept : Set State

  The set of accepting states.

@[implicit_reducible]

instance Cslib.Automata.DA.FinAcc.instAcceptor {State : Type u_1} {Symbol : Type u_2} : Acceptor (FinAcc State Symbol) Symbol

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.

Equations

• Cslib.Automata.DA.FinAcc.instAcceptor = { Accepts := fun (a : Cslib.Automata.DA.FinAcc State Symbol) (xs : List Symbol) => a.mtr a.start xs ∈ a.accept }

structure Cslib.Automata.DA.Buchi (State : Type u_3) (Symbol : Type u_4) extends Cslib.Automata.DA State Symbol : Type (max u_3 u_4)

Deterministic Buchi automaton.

• tr : State → Symbol → State
• start : State
• accept : Set State

  The set of accepting states.

@[implicit_reducible]

instance Cslib.Automata.DA.Buchi.instωAcceptor {State : Type u_1} {Symbol : Type u_2} : ωAcceptor (Buchi State Symbol) Symbol

An infinite run is accepting iff accepting states occur infinitely many times.

Equations

• Cslib.Automata.DA.Buchi.instωAcceptor = { Accepts := fun (a : Cslib.Automata.DA.Buchi State Symbol) (xs : Cslib.ωSequence Symbol) => ∃ᶠ (k : ℕ) in Filter.atTop, (a.run xs) k ∈ a.accept }

structure Cslib.Automata.DA.Muller (State : Type u_3) (Symbol : Type u_4) extends Cslib.Automata.DA State Symbol : Type (max u_3 u_4)

Deterministic Muller automaton.

• tr : State → Symbol → State
• start : State
• accept : Set (Set State)

  The set of sets of accepting states.

@[implicit_reducible]

instance Cslib.Automata.DA.Muller.instωAcceptor {State : Type u_1} {Symbol : Type u_2} : ωAcceptor (Muller State Symbol) Symbol

An infinite run is accepting iff the set of states that occur infinitely many times is one of the sets in accept.

Equations

• Cslib.Automata.DA.Muller.instωAcceptor = { Accepts := fun (a : Cslib.Automata.DA.Muller State Symbol) (xs : Cslib.ωSequence Symbol) => (a.run xs).infOcc ∈ a.accept }