Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller

TL;DR

This paper introduces a convex programming approach for synthesizing reset controllers in polynomial hybrid systems, ensuring safety and liveness properties through initial set computation and reset maps, demonstrated with practical examples.

Contribution

It presents a novel convex optimization-based method for reset controller synthesis in hybrid systems, addressing a gap in the current literature.

Findings

Method effectively synthesizes reset controllers for safety and liveness.

Approach reduces synthesis problems to convex optimization tasks.

Demonstrated efficiency and effectiveness through multiple examples.

Abstract

Controller synthesis, including reset controller, feedback controller, and switching logic controller, provides an essential mechanism to guarantee the correctness and reliability of hybrid systems in a correct-by-construction manner. Unfortunately, reset controller synthesis is still in an infant stage in the literature, although it makes theoretical and practical significance. In this paper, we propose a convex programming based method to synthesize reset controllers for polynomial hybrid systems subject to safety, possibly together with liveness. Such a problem essentially corresponds to computing an initial set of continuous states in each mode and a reset map associated with each discrete jump such that any trajectory starting from any computed initial state keeps safe if only safety constraints are given or reaches the target set eventually and keeps safe before that if both safety and liveness are given, through the computed reset maps. Both cases can be reduced to reach-avoid and/or differential invariant generation problems, further encoded as convex optimization problems. Finally, several examples are provided to demonstrate the efficiency and effectiveness of our method.