Formal Synthesis of Event-Triggered Controllers

Abstract

In networked control systems (NCS), the components of the control system communicate over a network, which poses challenges to the control synthesis procedure. Signal sampling is one of those challenges. A typical approach is to sample the signal periodically, but this can be inefficient. Event-triggered control (ETC) is a more efficient way to implement digital control for NCS because the control input is only recalculated when a triggering condition is violated. However, formal synthesis of event-triggered controllers is an open topic. In this work, we propose different methods to synthesize event-triggered controllers. The event-triggered controller consists of a triggering function based on a certificate function and a stabilizing feedback law. Counterexample-Guided Inductive Synthesis (CEGIS) is used to synthesize formally correct controllers. The feedback law is synthesized along with the certificate function or using feedback linearization. This framework is also extended to the synthesis of periodic event-triggered controllers, which periodically evaluate the triggering condition. A method is provided for how the sampling time of the triggering condition should be chosen. The synthesis approach is tested on several systems, through which the effectiveness of the approaches are demonstrated. It is shown that the method can synthesize event-triggered controllers for general nonlinear systems.