Finite Automata

Before we continue with the automatic property proof procedure -a proof checker- we have to clarify the assumption, that the model represented as a transition graph is representing a finite automaton.

The most simple definition of a finite automaton (FA) is as follows (cf. also figure 3.5):

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

with

1. $Q$ := Finite set of states
2. $I \subseteq Q$ := Set of initial states
3. $F \subseteq Q$ := Set of final states
4. $\Sigma$ := Finite set of symbols forming the alphabet
5. $\Delta \subseteq Q \times \Sigma \times Q$ := Set of transitions

Figure 3.5: Finite automaton, base version

A finite automaton $\cal A$ has a one-side tape T which holds a word w with $w \in \Sigma^{*}$ as a possible input. The input can be finite or infinite. The automaton can read the tape from a start position from 'left to right' without being able to go back. The read input is controlled by a set of finite states Q which are organized accordingly to the set $\Delta$. The computation of the input word w ends when the control unit $\langle Q,\Delta\rangle$ is entering a final state.

We can construct a finite automaton for the first transition graph $\cal G$ without properties $\Pi$ as follows:

1. $Q$ = $\{ 1,2,3,4 \}$
2. $I = \{ 1\}$
3. $F = \{ 4\}$
4. $\Delta$ $\subseteq$ $Q \times \Sigma^{*} \times Q$ with $\Delta$ = $\{\langle 1,A,2\rangle, \langle 1,B,1\rangle,\langle 1,C,1\rangle, \langle 2,A... ...C,1\rangle, \langle 3,A,4\rangle, \langle 3,B,1\rangle,\langle 3,C,1\rangle\}$
5. $\Sigma$ = $\{ A,B,C \}$

The execution of an automaton can also be understood as a sequence $\sigma_{\cal A}$ = $\langle\sigma_{0}, \sigma_{1}, \cdots, \sigma_{n}\rangle$, in this case as a sequence of automata configurations. Every element $\sigma_{i}$ of $\sigma_{\cal A}$ is an ordered pair $(q,w)$ of a state $q \in Q$ and the corresponding input word $w \in \Sigma^{*}$. If the position number $n$ of the last element is in the natural numbers $\cal N$ then $\sigma_{\cal A}$ is finite, otherwise infinite. For every two elements $\sigma_{i}$ and $\sigma_{i+1}$ of such an execution $\sigma_{\cal A}$ it holds, that $\langle proj1(\sigma_{i}), proj2(\sigma_{i}), proj1(\sigma_{i+1})\rangle \in \Delta$ and proj1( $\sigma_{0}$) $\in I$ and proj1( $\sigma_{n}$) $\in F$. The final element $\sigma_{n}$ with a final state $q \in F$ has as input word the empty word $\epsilon$.

Thus we could have the following execution sequence: $\sigma_{\cal A}$ = $\langle (1,B), (1,B), (1,C), (1,A), (2,B), (3,B), (1,A), (2,B), (3,A), (4,\epsilon) \rangle$

Using the execution sequence $\sigma_{\cal A}$ we can define two concepts: $stateSequence(\sigma_{\cal A}) = \langle proj1(\sigma_{0}), proj1(\sigma_{1}), \cdots, proj1(\sigma_{n})\rangle$ and $inputWord(\sigma_{\cal A}) = \langle proj2(\sigma_{0}), proj2(\sigma_{1}), \cdots, proj2(\sigma_{n})\rangle$. The stateSequence of an execution sequence provides all the states which are the basis for a path in the corresponding execution graph. The inputWord of an execution sequence is the sequence of all single words concatenated into one word.

Taking the execution sequence from above this would give us as a $stateSequence(\sigma_{\cal A})$ = $1,1,1,1, 2,3,1,2,3,4\rangle$ and as an $inputWord(\sigma_{\cal A})$= $\langle B,B,C,A,B,B, A,B,A,\epsilon \rangle$

We can then introduce the predicate $\vdash$ to represent an acceptance relation in the following way:

Def.: $\cal A$ $\vdash w$ iff there exists an execution sequence $\sigma_{\cal A}$ with $w = inputWord(\sigma_{\cal A})$

With this acceptance relation $\vdash$ we can then define the language $\cal L$ which will be accepted by an automaton $\cal A$:

Def.: $\cal L$ $_{\cal A}$ = $\{w\mid {\cal A} \vdash w \}$

Another helpful concept is the set of all possible execution sequences $\cal X$ of an automaton $\cal A$ in correspondence to the before introduced concept of an execution graph:

Def.: $\cal X_{\cal A}$ = $\{\sigma \mid \sigma is an execution sequence of automaton {\cal A}\}$