Signal (model checking)

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 functions from a set of real number to letters. This allow to use formalism similar to the ones of automata theory to deal with continuous signal.

Example

Consider an elevator. What is formally called a letter is could be in fact an information such that "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 of its buttons. The signal can then be analyzed by formal method 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 which allow to express time constraints.

A signal may be passed to a model, such as a signal automaton, which will decide, given the letters or actions which already occurred, what is the next action which should be done. 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.

Definition

Given an alphabet A, a signal ${\displaystyle \gamma }$ is a sequence ${\displaystyle (I_{0},a_{0}),(I_{1},a_{1}),\dots ,}$, finite or infinite, such that ${\displaystyle a_{i}\in A}$, each ${\displaystyle I_{i}\subseteq \mathbb {R} _{+}}$ are pairwise disjoint intervals, ${\displaystyle 0\in I_{0}}$, and ${\displaystyle I_{i}\cup I_{i+1}}$ is also an interval. Given ${\displaystyle t\in I_{i}}$ for some ${\displaystyle i}$, ${\displaystyle \gamma (t)}$ represents ${\displaystyle a_{i}}$.

Properties

Some authors restrict the kind of signals they considers. We list here some standard property that a signal may or may not satisfies.

Finite variability

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 time. In our previous elevator example, this property would means that a user may only press a button a finite number of time during a finite time. And similarly, in a finite time, the elevator can only opens and close its door a finite number of time.

Formally, a signal is said to have the finite variability property, unless the sequence is infinite and ${\displaystyle \bigcup _{i}I_{i}}$ is bounded. Intuitively, the finite variability property state that there is not an infinite number of change in a finite time. Having the finite variability property is similar to the notion of being non-Zeno for a timed word.[1]

Bounded variability

The notion of bounded variability is a restriction to the notion of finite variability. 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. Take the alphabet ${\displaystyle A=\{a,b\}}$. Take the interval ${\displaystyle \gamma }$ which sends the reals of the form ${\displaystyle n+{\frac {c}{n}}}$ with ${\displaystyle n\in \mathbb {N} }$ and ${\displaystyle c<n}$ to ${\displaystyle a}$ and every other reals to ${\displaystyle b}$. During each finite time interval, the letter change a finite number of time. Thus this signal is finitely variable. However, the distance between two successive occurrences of the letter ${\displaystyle a}$ is arbitrarily small. Thus it does not have the bounded variability property.

Let a sequence ${\displaystyle (I_{0},a_{0}),(I_{1},a_{1}),\dots }$. If ${\displaystyle a_{i}\neq a_{i+1}}$ for each integer ${\displaystyle i}$, then the sequence is said to have the bounded variability property if there exists a real ${\displaystyle r>0}$ such that, for each ${\displaystyle i<j}$ with ${\displaystyle a_{i}=a_{j}}$ such that there exists no ${\displaystyle k}$ with ${\displaystyle i<j<k}$ and ${\displaystyle a_{i}=a_{k}}$ then the difference between the lower bound of ${\displaystyle I_{j}}$ and of ${\displaystyle I_{i}}$ is at least ${\displaystyle r}$. Note that each sequence ${\displaystyle \gamma }$ is equivalent to a sequence ${\displaystyle \gamma '}$ in which two successive letters are distinct. The sequence ${\displaystyle \gamma }$ is said to have the bounded variability property if and only if ${\displaystyle \gamma '}$ has the bounded variability property.

A set of signal is said to has the bounded variability property if the above-mentioned lower bound ${\displaystyle r}$ can be chosen to be the same for each signal of the set.

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.

For example, for an arbitrary predicate ${\displaystyle e}$, the signal stating whether the statement "${\displaystyle p}$ holds sometime in the next time unit" holds has the bounded variability property. Indeed, when this statement becomes true, it remains true for a full time unit. Thus the difference between two occurrences where this statement becomes true is greater than a time unit.

Bipartite signal

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. And if the sequence alternate between singular intervals and open intervals.

Each signal is equivalent to a bipartite signal. Indeed, any interval which is closed on the left is the union of a singular interval and of an interval open on the left, in this order. And similarly for intervals closed on the right.

A signal automaton reading a bipartite signal has a special form. Its set of locations can be partitioned into locations for singular interval, and locations for open intervals. Each transition goes from a singular location to an open one and reciprocally.

See also

• Timed word

References

1. Brihaye, Thomas; Geeraerts, Gilles; Ho, Hsi-Ming; Monmege, Benjamin (2017). "Timed-Automata-Based Verification of MITL over Signals". International Symposium on Temporal Representation and Reasoning: 4.
2. Nickovic, Dejan (2008). "3". Checking Timed and Hybrid Properties: Theory and Applications (Thesis). p. 45.

• Kini, Dileep Raghunath; Krishna, Shankara Narayanan; Pandya, Paritosh K. (2011). "On construction of Safety Signal Automata for MITL[U,S] Using Temporal Projections". Formats: 227.