Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/7243
Title: State Equivalences for Rectangular Hybrid Automata
Authors: Henzinger, Thomas A.
Kopke, Peter W.
Keywords: computer science
technical report
Issue Date: Jul-1996
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR96-1588
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 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.
URI: http://hdl.handle.net/1813/7243
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
96-1588.pdf322.89 kBAdobe PDFView/Open
96-1588.ps332.41 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us