Finite Automata and Clocks

Intuitively is the above example directly 'understandable', but how can one fit all these expressions and operations into the framework of a finite automaton?

Let us have a look to the finite automaton with output, which we have introduced above (see also figure 3.6):

$$FA = \langle Q, I, F, \Sigma^{*}, \Xi^{*}, \Delta \rangle$$ (5.23)

$$\Delta \subseteq Q \times \Sigma^{*} \times \Xi^{*} \times Q$$ (5.24)

$$\delta = \langle q, in, out, q' \rangle$$ (5.25)

with the meaning that, if we have in state $q$ the input $in$, then we will generate the output $out$ and enter the successor state $q'$.

In the case of automata with properties $\Pi$ one can see how it is possible to extend the definition of an automaton by additional components which do not change the behavior of the automaton as such; the properties are only 'hooked up' to the structure of an automaton by providing some data 'viewable from a meta-level' only:

$$FA^{\Pi} = \langle Q, I, F, \Sigma^{*}, \Xi^{*}, \Delta, \lambda, \Pi \rangle$$ (5.26)

$$\Delta \subseteq Q \times \Sigma^{*} \times \Xi^{*} \times Q$$ (5.27)

$$\lambda : Q \longmapsto 2^{\Pi}$$ (5.28)

An analogous case could be to extend the basic FA-definiton with elements like time-points $T$, clocks $C$ as well as enabling conditions $\gamma$ like

$$FA^{\Pi,C} = \langle Q, I, F, \Sigma^{*}, \Xi^{*}, \Delta, \lambda, \Pi, T, \gamma,C \rangle$$ (5.29)

$$\Delta^{\Pi,C} \subseteq Q \times \Sigma^{*} \times C_{q} \times \gamma \times T \times \Xi^{*} \times Q$$ (5.30)

$$\lambda : Q \longmapsto 2^{\Pi}$$ (5.31)

$$\tau : Q \longmapsto 2^{C}$$ (5.32)

$$\gamma = \{=, <, >, \le, \ge\}$$ (5.33)

$$\delta = \langle q, in, c, g, t, out, q' \rangle$$ (5.34)

$$T \subseteq Rat$$ (5.35)

The $\Delta$ is usually called the transition relation of an automaton; another naming is machine table $MT$ or program. We will stick here with machine table $MT$ and we will name one element $\delta \in \Delta$ a command line of $MT$. The interpretation of a command line $\langle q, in, c, g, t, out, q' \rangle$ runs as ``while in state q an input-string 'in' will be received with the condition 'c,g,t' the output 'out' can be realized and the successor state is q' if the condition 'c,g,t' is satisfied. Otherwise this command line will not be executed.

If we call the two elements $\langle q_{r.j}, in_{q.r.j}\rangle$ of a command line $j$ the head of the command line than one can state that every head of the command lines of a state $q_{r} \in Q$ is unique. The uniqueness holds also for the tail of a command line which is represented by the elements $\langle out_{q.r.j}, q'_{q.r.j}\rangle$. The three elements $c_{q.r.j}, g_{q.r.j}, t_{q.r.j}$ of a command line $j$ will be called the clock condition.

One state $q \in Q$ can be realized by more than one command line, therefore it holds that

$$q = \{\delta\mid \delta \in \Delta \& \delta_{1} = q \}$$ (5.36)