Author(s):

Henzinger, Thomas A; Kopke, Peter W

Title: 
State equivalences for rectangular hybrid automata

Title Series: 
LNCS

Affiliation 

Abstract: 
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 timeabstract 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 RHA is equality (which obviously has an infinite quotient).
Our main positive result is established by analyzing a subclass of timed automata, called onesided timed automata (OTA), for which the language equivalence quotient is coarser than for the class of all timed automata. An exact characterization of language equivalence for OTA requires a distinction between synchronous and asynchronous definitions of (bi)simulation: if time actions are silent, then the induced quotient for OTA is coarser than if time actions (but not their durations) are visible.

Conference Title:

CONCUR: Concurrency Theory

Volume: 
1119

Conference Dates:

August 26–29, 1996

Conference Location:

Pisa, Italy

ISBN:

9783959770170

Publisher:

Schloss Dagstuhl  LeibnizZentrum für Informatik

Date Published:

19960101

Start Page: 
530

End Page:

545

DOI: 
10.1007/3540616047_74

Notes: 
This research was supported in part by ONR Young Investigator award N000149510520, by NSF CAREER award CCR9501708, by NSF grant CCR9504469, by Air Force Office of Scientific Research contract F496209310056, by ARPA grant NAG2892, and by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University, Contract Number DAAL0391C0027.

Open access: 
no 