Reset Controller Synthesis: A Correct-by-Construction Way to the Design of CPS

Abstract

Controller synthesis offers a correct-by-construction methodology to ensure the correctness and reliability of safety-critical cyber-physical systems (CPS). Controllers are classified based on the types of controls they employ, which include reset controllers, feedback controllers, and switching logic controllers. Reset controllers steer the behavior of a CPS to achieve system objectives by restricting its initial set and redefining its reset map associated with discrete jumps. Although the synthesis of feedback controllers and switching logic controllers has received considerable attention, research on reset controller synthesis is still in its early stages, despite its theoretical and practical significance. This paper outlines our recent efforts to address this gap. Our approach reduces the problem to computing differential invariants and reach-avoid sets. For polynomial CPS, the resulting problems can be solved by further reduction to convex optimizations. Moreover, considering the inevitable presence of time delays in CPS design, we further consider synthesizing reset controllers for CPS that incorporate delays.