Formal controller synthesis for hybrid systems using genetic programming

TL;DR

This paper introduces a novel framework that uses genetic programming to automatically synthesize controllers and Lyapunov-like functions for hybrid systems, enabling formal verification without polynomial restrictions.

Contribution

The proposed method allows automatic controller synthesis for general hybrid systems using genetic programming and SMT solvers, without requiring polynomial system assumptions.

Findings

Effective in nonpolynomial systems

Handles systems with uncertainties and jumps

Produces compact controller expressions

Abstract

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. We demonstrate the effectiveness of the proposed framework in several case studies, including nonpolynomial systems, sampled-data systems, systems with bounded uncertainties, switched systems, and systems with jumps. osed framework in several case studies, including nonpolynomial systems, sampled-data systems, systems with bounded uncertainties, switched systems, and systems with jumps.