## Polyhedral Flows in Hybrid Automata

*Rajeev Alur, Sampath Kannan, and Salvatore La Torre*
A *hybrid automaton* is a mathematical model for hybrid systems, which
combines, in a single formalism, automaton transitions for capturing
discrete updates with differential constraints for capturing continuous
flows. Formal verification of hybrid automata relies on symbolic
fixpoint computation procedures that manipulate sets of states.
These procedures can be implemented using
boolean combinations of linear constraints over
system variables, equivalently, using polyhedra,
for the subclass of *linear hybrid automata*.
In a linear hybrid automaton, the flow at each control mode
is given by a rate polytope that constrains the allowed
values of the first derivatives.
The key property of such a flow is that, given a state-set described
by a polyhedron, the set of states that can be reached as time elapses,
is also a polyhedron. We call such a flow a *polyhedral flow*.
In this paper, we study if we can generalize the syntax of linear hybrid
automata for describing flows without sacrificing the polyhedral property.
In particular, we consider flows described by *origin-dependent
rate polytopes*, in which the allowed rates depend, not only on the
current control mode, but also on the specific state at which the
mode was entered. We identify necessary and sufficient
conditions for a class of flows described
by origin-dependent rate polytopes to be polyhedral.
We also propose and study additional classes of flows:
{\em strongly polyhedral flows}, in which
the set of states that can be reached *upto a given time*
starting from a polyhedron is guaranteed to be a polyhedron, and
*polyhedrally-sliced flows*, in which
the set of states that can be reached *at a given time*
starting from a polyhedron is guaranteed to be a polyhedron.

*Hybrid Systems: Computation and Control,
Proceedings of the Second International Conference*,
(HSCC'99),
Lecture Notes in Computer Science 1569, pages 5--18,
Springer-Verlag, 1999.