Skip to main content


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

Please use this identifier to cite or link to this item:
Title: The Theory of Rectangular Hybrid Automata
Authors: Kopke, Peter W.
Keywords: computer science
technical report
Issue Date: Aug-1996
Publisher: Cornell University
Abstract: A {\em hybrid automaton\/} consists of a finite automaton interacting with a dynamical system. Hybrid automata are used to model embedded controllers and other systems that consist of interacting discrete and continuous components. A hybrid automaton is {\em rectangular\/} if each of its continuous variables~$x$ satisfies a nondeterministic differential equation of the form $a\le\frac{dx}{dt}\le b$, where $a$ and~$b$ are rational constants. Rectangular hybrid automata are particularly useful for the analysis of communication protocols in which local clocks have bounded drift, and for the conservative approximation of systems with more complex continuous behavior. We examine several verification problems on the class of rectangular hybrid automata, including reachability, temporal logic model checking, and controller synthesis. Both dense-time and discrete-time models are considered. We identify subclasses of rectangular hybrid automata for which these problems are decidable and give complexity analyses. An investigation of the structural properties of rectangular hybrid automata is undertaken. One method for proving the decidability of verification problems on infinite-state systems is to find finite quotient systems on which analysis can proceed. Three state-space equivalence relations with strong connections to temporal logic are bisimilarity, similarity, and language equivalence. We characterize the quotient spaces of rectangular hybrid automata with respect to these equivalence relations.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
96-1601.pdf1.69 MBAdobe PDFView/Open
96-1601.ps1.12 MBPostscriptView/Open

Refworks Export

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


© 2014 Cornell University Library Contact Us