## Discrete-Time Control for Rectangular Hybrid Automata

*
Thomas A. Henzinger
and Peter W. Kopke*

Rectangular hybrid automata model digital control programs of analog plant
environments.
We study rectangular hybrid automata where the plant state evolves
continuously in real-numbered time, and the controller samples the plant
state and changes the control state discretely, only at the integer points in
time.
We prove that rectangular hybrid automata have finite bisimilarity quotients
when all control transitions happen at integer times, even if the constraints
on the derivatives of the variables vary between control states.
This is in contrast with the conventional model where control transitions may
happen at any real time, and already the reachability problem is undecidable.
Based on the finite bisimilarity quotients, we give an exponential algorithm
for the symbolic sampling-controller synthesis of rectangular automata.
We show our algorithm to be optimal by proving the problem to be
EXPTIME-hard.
We also show that rectangular automata form a maximal class of systems for
which the sampling-controller synthesis problem can be solved
algorithmically.

*Theoretical Computer Science* 221:369-392, 1999.
A preliminary version appeared in the
*Proceedings of the
24th International Colloquium on Automata, Languages, and Programming*
(ICALP),
Lecture Notes in Computer Science 1256,
Springer, 1997, pp. 582-593.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1997 Springer,
1999 Elsevier.