Time and Temporal Operators

Because a run $ \varrho$ auf automaton A is a mapping from natural numbers into the set $ Q \times \Sigma^{*}$ one can use the domain dm($ \varrho$) as a model of time. In this view are the numbers elements of a time line, points of time. With regard to such a time line one can introduce operators talking about temporal properties.

There are four often used temporal operators X (next point of time), F (future, at some point in the following run, there will be a time), G (globally all points in that run, all the time), and U (until, from a certain point to some other point).

Gerd Doeben-Henisch 2010-03-03