We discuss various automata-theoretic formalisms for the specification and verification of real-time systems. We start with the general formalism of the hybrid automata as a model and specification language for hybrid systems. This is an extension of the traditional automata on infinite words in which the behavior of variables is governed in each state by a set of differential equations. Then we introduce the models of the timed automata and the integration graphs as special cases of the hybrid automata. We discuss the complexity of important verification issues related to the above models such as reachability and model-checking, and we survey the related algorithms.

Authors and Affiliations

1. Institute of Computer Science, FORTH and University of Crete, Greece

   Costas Courcoubetis

Editors and Affiliations

1. Department of Computer Systems, Uppsala University, P.O. Box 325, S-751 05, Uppsala, Sweden

   Bengt Jonsson

2. Swedish Institute of Computer Science, P.O. Box 1262, S-164 28, Kista, Sweden

   Joachim Parrow

Reprints and permissions

© 1994 Springer-Verlag Berlin Heidelberg

Policies and ethics