max planck institut

informatik

informatik

**MPI-I-1999-3-003**. August** **1999, 102 pages. | Status:** **available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

A specification formalism for reactive systems defines a class of

$\omega$-languages.

We call a specification formalism {\em fully decidable\/} if it is

constructively closed under boolean operations and has a decidable

satisfiability (nonemptiness) problem.

There are two important, robust classes of $\omega$-languages that are

definable by fully decidable formalisms.

The {\sc $\omega$-regular languages\/} are definable by finite automata,

or equivalently, by the Sequential Calculus.

The {\sc counter-free $\omega$-regular languages\/} are definable by

temporal logic, or equivalently, by the first-order fragment of the

Sequential Calculus.

The gap between both classes can be closed by finite counting

(using automata connectives), or equivalently, by projection

(existential second-order quantification over letters).

A specification formalism for real-time systems defines a class of

{\em timed\/} $\omega$-languages, whose letters have real-numbered time

stamps.

Two popular ways of specifying timing constraints rely on the use of

clocks,

and on the use of time bounds for temporal operators.

However, temporal logics with clocks or time bounds have undecidable

satisfiability problems, and finite automata with clocks

(so-called {\em timed automata\/}) are not closed under complement.

Therefore, two fully decidable restrictions of these formalisms have

been

proposed.

In the first case, clocks are restricted to {\em event clocks}, which

measure

distances to immediately preceding or succeeding events only.

In the second case, time bounds are restricted to {\em nonsingular

intervals},

which cannot specify the exact punctuality of events.

We show that the resulting classes of timed $\omega$-languages are

robust,

and we explain their relationship.

First, we show that temporal logic with event clocks defines the same

class

of timed $\omega$-languages as temporal logic with nonsingular time

bounds,

and we identify a first-order monadic theory that also defines this

class.

Second, we show that if the ability of finite counting is added to these

formalisms, we obtain the class of timed $\omega$-languages that are

definable by finite automata with event clocks, or equivalently, by a

restricted second-order extension of the monadic theory.

Third, we show that if projection is added, we obtain the class of timed

$\omega$-languages that are definable by timed automata, or

equivalently,

by the full second-order extension of the monadic theory.

These results identify three robust classes of timed $\omega$-languages,

of

which the third, while popular, is not definable by a fully decidable

formalism.

By contrast, the first two classes are definable by fully decidable

formalisms from temporal logic, from automata theory, and from monadic

logic.

Since the gap between these two classes can be closed by finite

counting, we

dub them the {\em timed $\omega$-regular languages\/} and the

{\em timed counter-free $\omega$-regular languages}, respectively.

Acknowledgement:** **

References to related material:

To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
---|---|

841 KBytes | |

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView |