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.

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.

##### MSC:

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.) |