Timed word

Consider an elevator. What is formally called a letter is could be in fact an information such that "someone press the button on the 2nd floor", or "the doors opened on the third floor". In this case, a timed word is a sequence of actions taken by the elevators and its users, with time stamps to recall those actions. The timed word 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 timed-word may be passed to a model, such as a timed 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 timed automaton and check the above mentioned property. That is, it will try to generate a timed-word 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.

Given an alphabet A, a timed word is a sequence, finite or infinite ${\displaystyle w=(a_{0},t_{0})(a_{1},t_{1})\dots }$ with ${\displaystyle a_{i}\in A}$, ${\displaystyle t_{i}\in \mathbb {R} _{+}}$ with ${\displaystyle t_{i}\leq t_{i+1}}$ for each integer ${\displaystyle i}$.

If the sequence is infinite but the sequence of ${\displaystyle (t_{0})(t_{1})\dots }$ is bounded, then this word is said to be a Zeno timed word,[1] in reference to the Zeno's paradoxes where an infinite number of action occurs in a finite time.

Untimed ${\displaystyle w}$ is the word ${\displaystyle w}$ without its time stamps, i.e. it is ${\displaystyle a_{0}a_{1}\dots }$. Given a timed language ${\displaystyle L}$, Untimed ${\displaystyle L}$ is then the set of untimed ${\displaystyle w}$ for ${\displaystyle w\in L}$.

• Alur, Rajeev; Dill, David (1994). "A theory of itmed automata". Theoretical Computer Science. 126: 190.