From Control Verification to Control Synthesis

To check if a hybrid system has a trajectory that leads to an error state, HYTECH searches backward from the error states to find all states that may lead to an error state. If, instead, one searches backward from a set of target states to find all states that must lead to a target state, one can automatically construct a control law that forces a system into a set of target states. This control technique has long been applied to discrete-event systems. We plan to extend the technique to hybrid modules, implement it in HYTECH, and study its relation to classical techniques for multi-modal control.

More precisely, let C be a hybrid module representing a multi-modal digital controller, and let P be a hybrid module representing the analog plant to be controlled. The set of safe states of P is called the target zone. There are several versions of the control problem for hybrid modules, with increasing degrees of difficulty:

Controller verification

Will all trajectories of the closed-loop system stay within the target zone?

Controller design

Construct a control module C such that all trajectories of stay within the target zone (or show that no such C exists).

Optimal control

Construct a control module C that minimizes a given cost function over all trajectories of  (for example, lead P as quickly as possible into the target zone).

We plan to proceed along three lines: (1) solve the controller verification problem for more complex differential inclusions and differential equations, perhaps under some helpful assumptions such as given sampling rates; (2) solve the controller design and optimal control problems, first for constant differential inclusions; (3) if a problem cannot be solved (formally decided), at least attempt to approximate a solution using both symbolic and numeric methods for analyzing differential equations. We will also address various formulations of the control problem that lie between pure analysis and full-fledged synthesis. For instance, the structure of the control module C could be given, while the values of certain parameters, such as cutoff values and sampling rates, need to be derived. Our algorithms will be implemented in HYTECH, which, for (3), must be linked with packages for symbolic and numeric computation.