## State Equivalences for Rectangular Hybrid Automata

*
Thomas A. Henzinger
and Peter W. Kopke*

Three natural equivalence relations on the infinite state space of a
hybrid automaton are language equivalence, simulation equivalence, and
bisimulation equivalence. When one of these equivalence relations has
a finite quotient, certain model-checking and controller-synthesis
problems are decidable. When bounds on the number of equivalence
classes are obtained, bounds on the running times of model checking
and synthesis algorithms follow as corollaries.

We characterize the time-abstract versions of these equivalence
relations on the state spaces of *rectangular hybrid automata*
(RHA), in which each continuous variable is a clock with bounded
drift. These automata are useful for modeling communications
protocols with drifting local clocks, and for the conservative
approximation of more complex hybrid systems. Of our two main
results, one has positive implications for automatic verification, and
the other has negative implications. On the positive side, we find
that the (finite) language-equivalence quotient for RHA is coarser
than was previously known by a multiplicative exponential factor. On
the negative side, we show that simulation equivalence for 3D RHA is
equality (which obviously has an infinite quotient).

Our main positive result is established by analyzing a subclass of
timed automata, called *one-sided timed automata* (OSA), for
which the language-equivalence quotient is coarser than for the class
all of timed automata. An exact characterization of language
equivalence for OSA requires a distinction between synchronous and
asynchronous definitions of (bi)simulation: if time actions are
silent, then the induced quotients for OSA (and thus RHA) are coarser
than if time actions (but not their durations) are visible.

*Proceedings of the
Seventh International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 1119,
Springer, 1996, pp. 530-545.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1996 Springer.