View source for Timed word

In [[model checking]], a subfield of [[computer science]], a '''timed word''' is an extension of the notion of words, in a [[formal language]], in which each letter is associated with a positive time tag. The sequence of time tags must be [[Non-decreasing function|non-decreasing]], which intuitively means that letters are received. For example, a system receiving a word over a network may associate to each letter the time at which the letter is received. The non-decreasing condition here means that the letters are received in the correct order.

A '''timed language'''{{anchor|Timed language}} is a set of timed words.

== Example ==
Consider an elevator. What is formally called a letter could be in fact information such as "someone pressed 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 methods]] to check whether a property such as "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 timed word may be passed to a model, such as a [[timed automaton]], which will decide, given the letters or actions that already occurred, what is the next action that 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.

== Definition ==
Given an [[Alphabet (formal languages)|alphabet]] ''A'', a timed word is a sequence, finite or infinite <math>w=(a_0,t_0)(a_1,t_1)\dots</math> with <math>a_i\in A</math>, <math>t_i\in\mathbb R_+</math> with <math>t_i\le t_{i+1}</math> for each integer <math>i</math>.

If the sequence is infinite but the sequence of <math>(t_0)(t_1)\dots</math> is bounded, then this word is said to be a '''Zeno timed word'''{{anchor|Zeno}},<ref name="Zeno">{{cite thesis |last=Estévenart |first=Morgane |date=September 2015 |title=Verification and synthesis of MITL through alternating timed automata |type=PhD |chapter=2|page=56}}</ref> in reference to [[Zeno's paradoxes]], where an infinite number of actions occur in a finite time.

The word <math>\operatorname{untimed}(w)</math>{{anchor|untimed}} is the word <math>w</math> without its time stamps, i.e. it is <math>a_0a_1\dots</math>. Given a timed language <math>L</math>, <math>\operatorname{untimed}(L)</math> is then the set of <math>\operatorname{untimed}(w)</math> for <math>w\in L</math>.

== References ==
<references />
* {{cite journal |last1=Alur |first1=Rajeev |last2=Dill |first2=David |author1link = Rajeev Alur| author2link = David L. Dill|title=A theory of timed automata |journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]] |date=1994|volume=126 |issue=2 |page=190|doi=10.1016/0304-3975(94)90010-8 |doi-access=free }}

{{DEFAULTSORT:Model Checking}}
[[Category:Model checking|*]]