EECS 298-11: CAD Seminar
Wednesday, February 26, 1997, 5pm
Cory Hall--Hogan Room

       Synthesizing Controllers for Linear Hybrid Automata

                        Howard Wong-Toi
                    Cadence Berkeley Labs


The design of an embedded digital device must consider the interaction
between the discrete behavior of the device and the analog behavior of
its physical environment.  Often the device consists of several
components, together with a controller for those components. It is
convenient to view the composition of the controlled components and
the physical environment as a hybrid plant. The synthesis problem is
to generate automatically a controller for a hybrid plant such that
their combined behavior meets a given safety constraint.

We present an algorithm for synthesizing finite-state controllers for
systems modeled as linear hybrid automata.  Our approach is based on
Maler et al.'s game-theoretic synthesis for timed systems.  The key
difficulty in the extension to hybrid systems is that the flow of the
continuous variables is nondeterministic in hybrid systems, as opposed
to deterministic in timed systems, and must be viewed as antagonistic
behavior by the plant.

The synthesis algorithm may generate controllers that are Zeno, i.e.
they cause the safety constraints to be satisfied by preventing time
from diverging.  We provide sufficient conditions on linear hybrid
automata under which any synthesized controller is guaranteed to be
nonZeno.

In many cases, the controller does not have complete observability of
the controlled environment.  Our algorithm is easily modified for
partial observability, at the cost of sacrificing completeness.  We
demonstrate the algorithm by synthesizing controllers for various
models of a steam-boiler.