Show simple item record

dc.contributor.authorKopke, Peter W.en_US
dc.description.abstractA {\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.en_US
dc.format.extent1727991 bytes
dc.format.extent1146587 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleThe Theory of Rectangular Hybrid Automataen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record