Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems

TL;DR

The paper tackles ensuring safety and reachability in delay hybrid systems through reset controller synthesis. It introduces a reach-avoid analysis for delay differential equations via a reach-avoid barrier functional (RABF) and reduces the synthesis problem to a convex SDP when dynamics are polynomial, followed by a mode-partitioned transformation into a discrete directed graph for tractable reset synthesis. The main contributions are an inner-approximation method for delay reach-avoid sets, a two-step discrete-graph-based reset synthesis framework, and a prototype implementation tested on nonlinear and benchmark delay-HS models, demonstrating robustness to larger delays. Practically, this approach enables correct-by-construction design of delay-aware hybrid controllers and provides a scalable pathway to verify and synthesize reset laws in CPS with time delays.

Abstract

A reset controller plays a crucial role in designing hybrid systems. It restricts the initial set and redefines the reset map associated with discrete transitions, in order to guarantee the system to achieve its objective. Reset controller synthesis, together with feedback controller synthesis and switching logic controller synthesis, provides a correct-by-construction approach to designing hybrid systems. However, time-delay is an inevitable factor in hybrid systems, which can degrade control performance and render verification certificates obtained by abstracting away time-delay invalid in practice. In this paper, we investigate this issue in a practical manner by taking time-delay into account. We propose an approach that reduces the synthesis of reset controllers to the generation of reach-avoid sets for the hybrid system under consideration, which can be efficiently solved using off-the-shell convex optimization solvers.

Figures (9)

• Figure 1: The dHA for hybrid delay damped oscillator
• Figure 2: Comparison between the method in xue2021reach and ours
• Figure 3: Mode partition of $q_1$. On the left side, we have mode $q_1$ with guard conditions $G(e_1)$ and $G(e_2)$ represented by blue slashes, and their intersection depicted by orange slashes. The reach-avoid set to $G(e_1) \cup G(e_2)$ can be partitioned into three disjoint regions: $g_{11}$, $g_{12}$, and $g_{13}$, as shown above. Accordingly, mode $q_1$ is partitioned into three sub-modes: $q_{11}$, $q_{12}$, and $q_{13}$.
• Figure 4: Mode partition of $q_3$. The left side is mode $q_3$ with the guard condition $G(e_3)$ (blue slashes) and the target set $T_{q_3}$ (green slashes). Correspondingly, $q_1$ is partitioned into two sub-modes: $q_{30}$ with $g_{30}=T_{q_3}$, and $q_{31}$ with $g_{31}=G(e_3)$.
• Figure 5: The resulting discrete directed graph