Automata, Languages, and Graphs

From the engineering framework we inherit the idea, that the key to the descriptipn of the expected behavior of required agents like user (U), environemnt (E) or technical system (S) is the description of the different individual interfaces understood as automata. This gives the concept of an automaton a pivotal role for the upcoming analysis. But the concept of an automaton has to be considered in close association to at least two other concepts: language and graph. Therefore we will give a short overview here about the conceptual network associated with the concept of an automaton.

Figure 5.1: Conceptual network related to Automata
\includegraphics[width=4.5in]{automata_grid.eps}

As you can see in figure 5.1 we will deal in this course with labeled finite automata, which can have a finite or infinite input. Depending from the kind of input we can observe finite or infinite runs of these automata. Automata can furthermore be understood as individual ones, disconnected from other automata, or they are connected with others, forming a network of parallel automata.

It is a widespread usage to present automata in a graphical representation called labelled transition graphs. The mapping from labelled finite automata to labelled transition graphs is straightforward (but you have to search very long to find an explicit definition in the literature...). For the purpose of verification one needs in many situations an explicit representation of all possible runs of an automaton. This can be given by an execution (or computation) graph. In cases of finite input will a finite automaton usually stops after finitely many operations. This is encoded in a transition graph by the fact, that there are final states as vertices without successors, these are called leaves. The same holds for execution graphs. Finite automata with infinite input will have infinite runs. This is encoded in a transition graph by the fact that there are no more final states, this means no more leaves. The same holds for execution graphs.

Because infinite runs can not be 'written down' neither as a run nor as a path one has to find appropriate descriptions of such infinite objekts.

Specifications given as logical expressions have to be checked against the execution graph. If all the paths of the graph are finite, then verifying the expressions is straightforward and also finite. If there is at least one infinite path, one has to find special devices to cope with such infinite objects.



Subsections
Gerd Doeben-Henisch 2010-03-03