Signal automaton
In automata theory, a field of computer science, a signal automaton is a finite automaton extended with a finite set of real-valued clocks.
During a run of a signal automaton, clock values increase all with the same speed.
Along the transitions of the automaton, clock values can be compared to integers.
These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviors of the automaton.
This language can be accepted by the automaton pictured nearby.As for finite automaton, incoming arrows represents initial locations and double circle represents accepting locations.
However, contrary to finite automata, letters occurs in locations and not in transition.
This is because letters are emitted continuously and transitions are taken discretely.
Note that the word state is thus ambiguous, since, depending on the author, it may means either a pair or an element of
For the sake of the clarity, this article will use the term location for element of
Here lies one of the biggest difference between signal-automata and finite automata.
In a finite automaton, at some point of the execution, the state is entirely described by the number of letter read and by a finite number of possible values, which are actually called "states".
That means that, given a state and a suffix of the word to read, the remaining of the run is totally determined.
However, as it is explained in the section "run" below, in order to resume clocks are used to determine which transitions can be taken.
Thus, in order to know the state of the automaton, you must both now in which location you are, and the clock valuation.
The letter is not determined by the transition but by the locations; this is due to the fact that the letters are emitted continuously while transitions are taken discretely.
The sequences are discrete but represents continuous events.
real: The signal defined by this run is the function
The notion of accepting run is defined as in finite automata for finite words and as in Büchi automata for infinite words.
As in the case of finite and Büchi automaton, a signal-automaton may be deterministic or non-deterministic.
It means that the set of start locations is a singleton, and that, given an extended state
Formally, this can be defined as follows: Depending on the authors, the exact definition of signal automata may be slightly different.
This restrict automata to accept only signals whose underlying partition satisfies the same property.
Rectangle states represents singular locations.
However, such a product is called a synchronization of automaton to emphasize the fact that the time should pass similarly in both automata considered.
The main difference between synchronization and product is that, when two finite automata read the same word, they take transition simultaneously.
This is not the case anymore for signal automata, since they can take transition at arbitrary time.
contains the following transitions: Timed automata is another extension of finite automata, which adds a notion of time to words.
In timed automata, letters are emitted on the transitions and not in the locations.
In timed automata, guards are only checked on transitions.
This simplifies the definition of deterministic automaton, since it means that the constraint must be satisfied before the clocks are restarted.
