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

with

- := Finite set of states
- := Set of initial states
- := Set of final states
- := Finite set of symbols forming the alphabet
- := Set of transitions

A finite automaton has a one-side tape T which holds a word w with 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 . The computation of the input word w ends when the control unit is entering a final state.

We can construct a finite automaton for the first transition graph without properties as follows:

- =
- with =
- =

The execution of an automaton can also be understood as a sequence = , in this case as a sequence of automata configurations. Every element of is an ordered pair of a state and the corresponding input word . If the position number of the last element is in the natural numbers then is finite, otherwise infinite. For every two elements and of such an execution it holds, that and proj1( ) and proj1( ) . The final element with a final state has as input word the empty word .

Thus we could have the following execution sequence: =

Using the execution sequence we can define two concepts: and . 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 = and as an =

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

Def.: iff there exists an execution sequence with

With this acceptance relation we can then define the language which will be accepted by an automaton :

Def.: =

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

Def.: =

Gerd Doeben-Henisch 2010-03-03