In model checking, a subfield of computer science, a signal or timed state sequence is an extension of the notion of words in a formal language, in which letters are continuously emitted.
While a word is traditionally defined as a function from a set of non-negative integers to letters, a signal is a function from a set of real numbers to letters.
This allow the use of formalisms similar to the ones of automata theory to deal with continuous signals.
What is formally called a letter could be in fact information such as "someone is pressing the button on the 2nd floor", or "the doors are currently open on the third floor".
In this case, a signal indicates, at each time, which is the current state of the elevator and its buttons.
The signal can then be analyzed using formal methods to check whether a property such that "each time the elevator is called, it arrives in less than three minutes, assuming that no one held the door for more than fifteen seconds" holds.
A statement such as this one is usually expressed in metric temporal logic, an extension of linear temporal logic that allows the expression of time constraints.
A signal may be passed to a model, such as a signal automaton, which will decide, given the letters or actions that already occurred, what is the next action that should be performed, in our example, to which floor the elevator must go.
Then a program may test this signal and check the above-mentioned property.
That is, it will try to generate a signal in which the door is never held open for more than fifteen seconds, and in which a user must wait more than three minutes after calling the elevator.
Some authors restrict the kind of signals they consider.
We list here some standard properties that a signal may or may not satisfy.
Intuitively, a signal is said to be finitely variable, or to have the finite variability property, if during each bounded interval, the letter change a finite number of times.
In our previous elevator example, this property would mean that a user may only press a button a finite number of times during a finite time.
And similarly, in a finite time, the elevator can only open and close its door a finite number of times.
Formally, a signal is said to have the finite variability property, unless the sequence is infinite and
Intuitively, the finite variability property states that there is not an infinite number of changes in a finite time.
Having the finite variability property is similar to the notion of being non-Zeno for a timed word.
A signal has the bounded variability property if there exists a lower bound between the beginning of two intervals with the same letter.
[2] Before giving a formal definition, we give an example of signal which is finitely variable but not boundedly variable.
During each finite time interval, the letter changes a finite number of times.
However, the distance between two successive occurrences of the letter
, then the sequence is said to have the bounded variability property if there exists a real
We know give main reason to consider signals with bounded variabilities.
Assume we need to create a system, such as a signal automaton, which need to recall everything which occurred in the last time units.
If we know that the signal is boundedly variable, we can compute an upper bound on the number of action which occurred during one time unit.
Thus, we can create such a system and ensure that it only requires a finite memory.
Thus the difference between two occurrences where this statement becomes true is greater than a time unit.
A signal is said to be bipartite if the sequence of intervals start with a singular interval – i.e. a closed interval whose lower and upper bound are equal, hence a set which is a singleton.
Each transition goes from a singular location to an open one and reciprocally.