Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation

TL;DR

This paper presents a method for synthesizing switching controllers for hybrid systems by generating continuous invariants using quantifier elimination and sum-of-squares techniques, reducing human effort and computational complexity.

Contribution

It introduces a combined approach using QE-based and SOS relaxation methods for invariant generation, enhancing automation and efficiency in hybrid system control synthesis.

Findings

Effective invariant generation with reduced human interaction.

Application of SOS relaxation improves computational efficiency.

Method achieves relative completeness within predefined templates.

Abstract

We extend a template-based approach for synthesizing switching controllers for semi-algebraic hybrid systems, in which all expressions are polynomials. This is achieved by combining a QE (quantifier elimination)-based method for generating continuous invariants with a qualitative approach for predefining templates. Our synthesis method is relatively complete with regard to a given family of predefined templates. Using qualitative analysis, we discuss heuristics to reduce the numbers of parameters appearing in the templates. To avoid too much human interaction in choosing templates as well as the high computational complexity caused by QE, we further investigate applications of the SOS (sum-of-squares) relaxation approach and the template polyhedra approach in continuous invariant generation, which are both well supported by efficient numerical solvers.