2020/03/31 by Cees F. Verdier, Verdier, Cees F., Manuel Mazo +2
Computer Science · Engineering · #Advanced Control Systems Optimization #Evolutionary Algorithms and Applications #FOS: Electrical engineering #Formal Methods in Verification #Systems and Control (eess.SY) #cs.SY #eess.SY #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2003.14322
Revised version (9/15/2020)
openalex publication_date 2020/03/31 · arxiv created 2020/09/15 · arxiv updated 2020/09/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.