timed word

In model checking, timed word is an extension of the notion of words, in which each letter is associated with a positive time tag. The sequence of time tag must be 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 is a set of timed words.

Given an alphabet A, a timed word is a sequence, finite or infinite $w=(a_0,t_0)(a_1,t_1)\dots$ with $a_i\in A$，$t_i\in {\mathbb{R}}_{+}$ with $t_i\le t_{i+1}$ for each integer $i$.

If the sequence is infinite but the sequence of $(t_0)(t_1)\dots$ is bounded, then this word is said to be a Zeno timed word in reference to the Zeno’s paradoxes where an infinite number of action occurs in a finite time.

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