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

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 at cycle time (usually '1' for the beginning, can be also '0') and a state counter . If is a start state with then 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 all clocks connected to states have to be set to zero '0'.

1. Reading: The content of the actual tape cell will be read at position as an input string with as the cycle number.
2. Matching the Input: The actual state will be matched with regard to the actual input by looking for a command line with the unique head .
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 of state in command line -abbreviated as - satisfies the relation given by the relation and the constant . This check is a simple boolean operation which yields true or false.
1. true: then the clock will be set back to '-1', the output will be written onto the tape at position and the state counter will be set to the follow-up state .
2. false: if the clock does not match, then there are two more options:
1. No Satisfaction Possible: The condition will never become satisfied in the future because the clock has already a value beyond the constant . 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 has a value which actually is below the constant and can possibly become satisfied in the future. No output is written. The follow-up state is not realized. stays unchanged.
5. Preparing Next Cycle : The system clock and all clocks 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 with .
2. An actual state announced by the .
3. The head of one of the command lines of the state matching the input.
4. The clock condition of that command line which at least possibly becomes true or either is satisfied.
5. An output if intended.
6. The follow-up state . 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 stays unchanged.

Thus we get the following line:

A complete run of an automaton based on a sequence of input events is then a sequence such that .

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 . 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 can then be defined as

. A direct transition between two consecutive elements of a run can be written as

.

For a run of an automaton we can also describe an element, which is reachable at position in as

where it holds that .

The set of all reachable heads can then be defined as

Gerd Doeben-Henisch 2010-03-03