Formal controller synthesis for hybrid systems using genetic programming

Understand

This paper proposes a framework for automatic formal controller synthesis for general hybrid systems with a subset of safety and reachability specifications.

• The framework uses genetic programming to automatically co-synthesize controllers and candidate Lyapunov-like functions.
• These candidate Lyapunov-like functions are used to formally verify the control specification, and their correctness is proven using a Satisfiability Modulo Theories solver.
• The advantages of this approach are: no restriction is made to polynomial systems, the synthesized controllers are expressed as compact expressions, and no explicit solution structure has to be specified beforehand.