Henzinger, Thomas A.Kopke, Peter W.2007-04-232007-04-231996-07http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR96-1588https://hdl.handle.net/1813/7243Three 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 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 quotient for OSA is coarser than if time actions are visible.330640 bytes340390 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report