zbMATH — the first resource for mathematics

Automata for modeling real-time systems. (English) Zbl 0765.68150
Automata, languages and programming, Proc. 17th Int. Colloq., Warwick/GB 1990, Lect. Notes Comput. Sci. 443, 322-335 (1990).
Summary: [For the entire collection see Zbl 0758.00017.]
We show that the class of languages accepted by timed Büchi automata (TBA) is closed under the operations of union, intersection and projections, and the trace language obtained by projecting the language accepted by a TBA is \(\omega\)-regular. It turns out that TBAs are not closed under complement,and it is undecidable whether the language of one automaton is a subset of the language of another. This result is an obstruction to automatic verification. However, we show that a significant (proper) subclass represented by deterministic timed Muller automata (DTMA) is closed under all the Boolean operations. Consequently, a system modeled by a TBA can be automatically verified with respect to a specification given as a DTMA.

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)