Abstract-- 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 trajectorybased 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 con...
A. Agung Julius, Sina Afshari