Finite Labelled Automaton

For the verification task later on it is necessary, that we can associate each state with a finite set of properties. This can be done with a labelling function l:

Definition: An A is a labelled finite automaton (LFA) iff it is a tuple

$$\langle Q,I, F, \Sigma, \Delta, l, AP \rangle$$

with

1. Q is a finite set of states
2. I $\subseteq$ Q is the set of initial states
3. F $\subseteq$ Q is the set of final states
4. $\Sigma$ is an input alphabet
5. $\Delta$ $\subseteq$ Q $\times$ $\Sigma^{*}$ $\times$ Q is the set of transitions
6. AP is a finite set of atomic propositions
7. $l: Q \longrightarrow 2^{AP}$ /* Associates each state with a finite set of propositions */