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

structure Cslib.FLTS (State : Type u_1) (Label : Type u_2) : Type (max u_1 u_2)

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).

• tr : State → Label → State

  The transition function.

def Cslib.FLTS.mtr {State : Type u_1} {Label : Type u_2} (flts : FLTS State Label) (s : State) (μs : List Label) : State

Extended transition function.

Implementation note: compared to [HMU06], the definition consumes the input list of symbols from the left (instead of the right), in order to match the way lists are constructed.

Equations

• flts.mtr s μs = List.foldl flts.tr s μs

@[simp]

theorem Cslib.FLTS.mtr_nil_eq {State : Type u_1} {Label : Type u_2} {flts : FLTS State Label} {s : State} : flts.mtr s [] = s

@[simp]

theorem Cslib.FLTS.mtr_concat_eq {State : Type u_1} {Label : Type u_2} {flts : FLTS State Label} {s : State} {μs : List Label} {μ : Label} : flts.mtr s (μs ++ [μ]) = flts.tr (flts.mtr s μs) μ

theorem Cslib.FLTS.mtr_append_eq {State : Type u_1} {Label : Type u_2} {flts : FLTS State Label} {s : State} {μs1 μs2 : List Label} : flts.mtr s (μs1 ++ μs2) = flts.mtr (flts.mtr s μs1) μs2