A Unified Game Theoretic Approach to Synthesis of Multi-modal Control Laws

In some recent work [38], we have shown that it is important to have a unified approach to the treatment of methods from control, and computer science. Here is an alphabet table in this regard: Let denote the space of piecewise continuous functions over , and the space of piecewise differentiable functions over .

With this sort of an identification, we are able to show that synthesis problems for hybrid conditions with so-called safety specifications, i.e. those for which the acceptance conditions are may be solved under conditions of tremendous generality for non-linear hybrid automata by using Hamilton Jacobi equations, and an algorithmic construction for the maximal safe sets and least restrictive control laws. The Hamilton Jacobi equation (and its discrete counterpart) is a partial differential equation of the form

where is the so-called Hamiltonian determined from the appropriate target sets and the game between the controllable and uncontrollable actions (or between the software and the data). This approach is very much in the spirit of Church, Büchi, Landweber and Rabin for discrete games on automata.

The following open problems need to be addressed to convert this general approach into a automated synthesis procedure:

Numerical Solutions of Hamilton Jacobi Equations

Since the synthesis procedure described above is general, its utility depends on the availability of efficient numerical tools for computing its solutions. Approximation techniques are a first step, here there will be connections with the linear hybrid automata approach of HYTECH. In addition, we will quantitative methods for computing when the equation has shocks, corresponding to changes in the gaming strategy, This has connections with modern mathematically theory of wavefront propagation and viscosity solutions of Hamilton Jacobi Equations.

Hierarchical Solutions of Synthesis Procedures

For systems with high dimensional state spaces or for many agents, a hierarchical application of the approach is necessary to facilitate the computations associated with safety and least restrictive control computations.

Liveness and Other Acceptance Conditions

Liveness, fairness and other acceptance conditions such as , are important to model in the framework described for safety games, not just for mathematical completeness, but also to be able to establish the fairness of certain synthesized solutions for multi-agent problems. We believe that this is possible not by nested Hamilton Jacobi solutions, but by a single new Hamiltonian.

Probabilistic Synthesis Techniques

As in the verification subsection to follow, viscosity solutions to Hamilton Jacobi equations give an indication that probabilistic synthesis techniques are important to study. Thus, the usual deterministic acceptance conditions , etc. need to be replaced by probabilistic ones, to guarantee safety to within a certain tolerance.