Using computer games for hybrid systems controller synthesis

We propose a formal method for feedback controller synthesis using interactive computer programs with graphical interface (in short, computer games). The main theoretical tool used in this method is the concept of trajectory robustness, which is established using the theory of approximate bisimulation. Approximate bisimulation has been used to establish robustness (in ℓ_∞ sense) of execution trajectories of dynamical systems and hybrid systems, resulting in trajectory-based safety verification procedures. We define control autobisimulation function (CAF), which is the analog of control Lyapunov function for approximate bisimulation. CAF is used to characterize the family of all feedback control laws, called admissible control laws, that result in a close loop system with an autobisimulation function. A computer game can then be used to construct safe and correct execution trajectory for a nominal initial state, and use the trajectory-robustness property to guarantee that the control law is also safe for other initial states in a neighborhood of the nominal initial state. As a result, a safe and correct feedback control law for a compact noncountable set of initial states can be obtained by playing finitely many games.