Nondeterministic Automaton

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

structure Cslib.Automata.NA (State : Type u_1) (Symbol : Type u_2) extends Cslib.LTS State Symbol : Type (max u_1 u_2)

A nondeterministic automaton extends a LTS with a set of initial states.

• Tr : State → Symbol → State → Prop
• start : Set State

  The set of initial states of the automaton.

def Cslib.Automata.NA.Run {State : Type u_1} {Symbol : Type u_2} (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) : Prop

Infinite run.

Equations

• na.Run xs ss = (ss 0 ∈ na.start ∧ ∀ (n : ℕ), na.Tr (ss n) (xs n) (ss (n + 1)))

theorem Cslib.Automata.NA.Run.mk {State : Type u_1} {Symbol : Type u_2} {na : NA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} (h₁ : ss 0 ∈ na.start) (h₂ : ∀ (n : ℕ), na.Tr (ss n) (xs n) (ss (n + 1))) : na.Run xs ss

theorem Cslib.Automata.NA.Run.start {State : Type u_1} {Symbol : Type u_2} {na : NA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} (run : na.Run xs ss) : ss 0 ∈ na.start

theorem Cslib.Automata.NA.Run.trans {State : Type u_1} {Symbol : Type u_2} {na : NA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} (run : na.Run xs ss) (n : ℕ) : na.Tr (ss n) (xs n) (ss (n + 1))

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

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

• Tr : State → Symbol → State → Prop
• start : Set State
• accept : Set State

  The set of accepting states.

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

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.

Equations

• Cslib.Automata.NA.FinAcc.instAcceptor = { Accepts := fun (a : Cslib.Automata.NA.FinAcc State Symbol) (xs : List Symbol) => ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s' }

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

Nondeterministic Buchi automaton.

• Tr : State → Symbol → State → Prop
• start : Set State
• accept : Set State

  The set of accepting states.

instance Cslib.Automata.NA.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

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

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

Nondeterministic Muller automaton.

• Tr : State → Symbol → State → Prop
• start : Set State
• accept : Set (Set State)

  The set of sets of accepting states.

instance Cslib.Automata.NA.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

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