Automata Theoretic Semantics of Time

The usual way to give the semantics of an automata theoretic structure is to describe the execution of such a structure as a run (cf. figure 5.5).

Figure 5.5: Timed Automata Semantics as Execution

Whether we have a deterministic or an indeterministic version of an automaton it does not matter: in every execution cycle only one command line will be executed.

An execution cycle is to be understood as an operation where we have an automaton $a$ at cycle time $CLCK_{a} =i$ (usually '1' for the beginning, can be also '0') and a state counter $MTC = q_{r}$. If $q_{r}$ is a start state with $r=1$ then $q_{r} \in I$^5.1. The tape starts with position '1' (or '0') with one section for reading and one for writing and can be infinite. In the beginning $CLCK_{a} =1$ all clocks $C$ connected to states have to be set to zero '0'.

1. Reading: The content of the actual tape cell will be read at position $i = CLCK_{a}$ as an input string $in_{i}$ with $i$ as the cycle number.
2. Matching the Input: The actual state $q_{r} = MTC$ will be matched with regard to the actual input $in_{i}$ by looking for a command line $j$ with the unique head $q_{r}, in_{i}$.
3. Decision: If the actual state does not match then the automaton stops (here an error message could be foreseen). Otherwise the cycle continues.
4. Matching the Clock: It has to be checked whether the actual value of the clock $c$ of state $q_{r}$ in command line $j$ -abbreviated as $c_{q.r.j}$- satisfies the relation given by the relation $g_{q.r.j}$ and the constant $t_{q.r.j}$. This check is a simple boolean operation which yields true or false.
   1. true: then the clock $c_{q.r.j}$ will be set back to '-1', the output $out_{q.r.j}$ will be written onto the tape at position $i$ and the state counter $MTC$ will be set to the follow-up state $q'_{q.r.j}$.
   2. false: if the clock $c_{q.r.j}$ does not match, then there are two more options:
      1. No Satisfaction Possible: The condition $c_{q.r.j}, g_{q.r.j}, t_{q.r.j}$ will never become satisfied in the future because the clock $c_{q.r.j}$ has already a value beyond the constant $t_{q.r.j}$. This is a simple boolean operation. The actual state does not match and the automaton stops (here an error message could be foreseen).
      2. Satisfaction Is Possible: the clock $c_{q.r.j}$ has a value which actually is below the constant $t_{q.r.j}$ and can possibly become satisfied in the future. No output is written. The follow-up state is not realized. $MTC$ stays unchanged.
5. Preparing Next Cycle : The system clock $CLCK_{a}$ and all clocks $C$ connected to states will be incremented by one. Go to Reading again.

A simple version of a run -or an execution- of an automaton can then be interpreted as a protocol of the cycles described above. The statement of each cycle which does not cause an error contains the following elements:

1. An input $in_{i}$ with $i = CLCK_{a}$.
2. An actual state $q_{r}$ announced by the $MTC$.
3. The head of one of the command lines $j$ of the state $q_{r}$ matching the input.
4. The clock condition $c_{q.r.j}, g_{q.r.j}, t_{q.r.j}$ of that command line $j$ which at least possibly becomes true or either is satisfied.
5. An output $out_{q.r.j}$ if intended.
6. The follow-up state $q'_{q.r.j}$. The follow-up state can be suppressed under the special condition that a clock has not yet reached the required value. In this situation the $MTC$ stays unchanged.

Thus we get the following line:

$i \Longrightarrow q_{r}, in_{q.r.j}, c_{q.r.j}, g_{q.r.j}, t_{q.r.j}, out_{q.r.j}, \{q_{r}\} \cup \{q'_{q.r.j}\}$

A complete run $\varrho_{a}$ of an automaton $a$ based on a sequence of input events $in = in_{1}, in_{2}, \cdots, in_{k}$ is then a sequence $\varrho_{a} = \varrho_{a.1}\varrho_{a.2}...\varrho_{a.k}...$ such that $\varrho_{k} = q_{r}, in_{q.r.j}, c_{q.r.j}, g_{q.r.j}, t_{q.r.j}, out_{q.r.j}, \{q_{r}\} \cup \{q'_{q.r.j}\}$.

In this version is a timed automaton a different automaton compared to the usual finite automaton! The execution of the automaton not only examines whether a certain state q and a certain input 'in' is given, but additionally whether the clock c has a certain value and that this value satisfies a condition $\gamma T$. If the input 'in' is given but the clock does not satisfy the condition, then the operation will not be executed. This changes the behavior of a timed finite automaton compared to an 'usual' finite automaton.

The set of all possible executions of a finite automaton a $EXEC_{a}$ can then be defined as

$$EXEC_{a} = \{x \mid x = \varrho_{a} \}$$

. A direct transition between two consecutive elements $(\varrho_{a.i}, \varrho_{a.i+1})$ of a run $\varrho_{a}$ can be written as

$$\varrho_{a.i} \longrightarrow \varrho_{a.i+1}$$

.

For a run $\varrho_{a}$ of an automaton $a$ we can also describe an element, which is reachable at position $k$ in $\varrho_{a}$ as

$$\varrho \vdash \varrho_{k}$$

where it holds that $\forall(0 < j \le k)\exists(i) (\varrho_{i} \longrightarrow \varrho_{j})$.

The set of all reachable heads can then be defined as

$$Reachable_{a} = \{(q,in) \mid \exists(\varrho, k)(\varrho \vdash \varrho_{k} \& (q,in) = headof(\varrho_{k} )\}$$