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.

Introduction

As defined by Baheti and Gill (2011), cyber-physical systems (CPS) refers to a new generation of systems integrating computational and physical capabilities, capable of interacting with humans through various modalities. The ability to interact with, and expand the capabilities of, the physical world through computation, communication and control serves as an enabler for future technology developments. CPS is pervasive in our daily life, examples include spacecrafts, high speed train control systems, automated plants and factories and so on. Many of these systems are entrusted with safety-critical tasks, necessitating the development of formally verifiable CPS that are both safe and reliable. However, efficiently developing such CPS remains a longstanding challenge.

Controller synthesis provides a correct-by-construction mechanism to guarantee the correctness and reliability of CPS. In essence, controller synthesis endeavors to create an operational behavior model for a component, based on a model of assumed environmental behaviors and a system goal. This process ensures the system reliably achieves the specified objective when the environment aligns with the provided assumptions. Controller synthesis has attracted increasing attention from computer science and control theory in the past decades. In the case of CPS, an operation (i.e., control) could be either an input to dynamics, a switch condition from one mode to another, an initial condition for each mode, or a reset map when conducting discrete jumps. Depending on the types of controls, controllers can be naturally classified into feedback controllers, switching logic controllers and reset controllers. In the literature, there is a huge bulk of work on the synthesis of controllers of the first two types, please refer to (Tomlin et al. 2000; Asarin et al. 2000; Coogan and Arcak 2012; Jha et al. 2010; Taly, Gulwani, and Tiwari 2011; Girard 2012; Gulwani and Tiwari 2008; Taly, Gulwani, and Tiwari 2011; Zhao, Zhan, and Kapur 2013) and the references therein. However, the synthesis of controllers of the third type is still in the infant stage, despite its theoretical and practical significance. Many important practical problems can be reduced to reset controller synthesis, e.g., the substantial instantaneous change in velocity of a spacecraft induced by impulsive controls in satellite rendezvous (Brentari et al. 2018), re-configuring safety-critical devices such as spacecraft when an exception happens, etc. Furthermore, as indicated by the following motivating example, in some cases, the system goal cannot be achieved only with feedback controllers and/or switching logic controllers.

Figure 1. Hybrid Automaton for Example 1.

Example 1 (A motivating example (Liu et al. 2023)). Consider a CPS given in Figure 1.

Suppose the safe sets in mode ${q_1}$ and ${q_2}$ are ${{\cal S}_1} = \left[ {15,31} \right)$ , ${{\cal S}_2} = \left( {0,14} \right]$ , respectively. As the dynamics in the two modes both are autonomous without inputs, it is impossible to find feedback controllers for them to maintain safety. Moreover, one may easily observe that once a discrete jump happens, the system will not be safe anymore. This means only strengthening the domain constraints and guards for discrete jumps to maintain safety is trivially impossible. However, it is possible to synthesize a reset controller to maintain safety.

Related work

Numerous studies have delved into verifying hybrid systems, which can broadly be categorized into model-checking and theorem proving. The former is essentially based on reachable set computation, currently can only handle bounded time. For example, tools such as SpaceEx (Frehse et al. 2011), iSAT-ODE (Eggers, Fränzle, and Herde 2008), dReach (Kong et al. 2015) and Flow* (Chen, Ábrahám, and Sankaranarayanan 2013) fall within this category. In contrast, the latter can provide unbounded verification of HSs with scalability based on specification logics and invariant generation, e.g., differential dynamic Logic (dL) (Platzer 2012) and hyrid Hoare logic (HHL) (Liu et al. 2010; Zhan et al. 2023). dL demonstrates significant capability in deducing verification for HSs, proving effective across various verification challenges, including the verification of liveness properties (Tan and Platzer 2019) and switched systems (Tan and Platzer 2021) with the help of the tool KeYmaera X (Platzer 2010). While, HHL can handle more complicated behaviors of HSs such as communication, concurrency and so on, with the help of the tool HHLProver (Wang, Zhan, and Zou 2015). Event-B (Richard 2024; Richard et al. 2017; Richard et al. 2015; Butler, Abrial, and Banach 2016; Dupont et al. 2021; Dupont et al. 2022) also stands as a useful method for formal modeling and verifying HSs.

Verification of HSs can also be pursued in a correct-by-construction manner through refinement syntactically (Back and Wright 2012) or controller synthesis semantically (Bozga and Sifakis 2022). Refinement plays a key role in classical programming theories, however, the counterparts for HSs are really few in the literature, although model-based design has become dominant in the design of HSs. Loos and Platzer (2016) proposed differential refinement logic to cope with refinement relation among different levels of abstraction for a given HS. Yan et al. (2020) defined a set of refinement rules for transforming HCSP to System C, and Wang et al. (2024) proposed a set of refinement rules for transforming HCSP to ANSI-C, both with the correctness guarantee based on approximate bisimulation.

Extensive work has been dedicated to controller synthesis for HSs. One category of research focuses on feedback controllers, with various methods addressing this type of synthesis problem, including moment-based methods (Zhao, Mohan, and Vasudevan 2019), Hamilton-Jacobi-based methods (Tomlin, Lygeros, and Sastry 2000), barrier certificates-based methods (Ames et al. 2016), abstraction-based methods (Girard 2012), and counter-example-guided inductive synthesis methods (Abate et al. 2017). Another category addresses the synthesis problem of switching controllers, which can be classified into abstraction-based methods (Girard 2012; Tabuada 2009; Belta, Yordanov, and Gol 2017) and constraint-solvingbased methods (Taly, Gulwani, and Tiwari 2011; Zhao, Zhan, and Kapur 2013; Taly and Tiwari 2010). However, since its initial exploration in Clegg (1958), there has been limited research on reset controllers, which is the focus of our paper.

Synopsis of reset controller synthesis

In this paper, we summarize our recent work on the reset controller synthesis for CPS, details can be found in Liu et al. (2023) and Su et al. (2023).

Reset controller synthesis without time delay

Firstly, we investigate reset controller synthesis with ideal mathematical models, i.e., hybrid automata (HA), which is a popular model for CPS. Formally,

Definition 1 An HA ${\cal H}$ is a tuple $\left( {{\cal Q},{\cal X},f,Init,Dom,{\cal E},{\cal G},{\cal R}} \right)$ , where

• ${\cal Q} = \left\{ {{q_1},{q_2}, \ldots } \right\}$ is a finite set of modes;

• $X = \left\{ {{x_1}, \ldots, {x_n}} \right\}$ is a set of continuous state variables, also written as a vector of variables ${\bf{x}}$ , which is interpreted over ${{\mathbb{R}}^n}$ . Normally, we use ${\cal X} \subseteq {{\mathbb{R}}^n}$ to denote the continuous state space, and a (hybrid) state of the system is represented as $\left( {q,{\bf{x}}} \right) \in {\cal Q} \times {\cal X}$ ;

• ${\rm{Init}} \subseteq {\cal Q} \times {\cal X}$ is a set of initial states;

• ${\rm{Dom}}:{\cal Q} \to P\left( {\cal X} \right)$ assigns to each $q \in {\cal Q}$ a domain, written as ${\rm{Do}}{{\rm{m}}_q} \subseteq {\cal X}$ . The system can reside in a mode only if the domain constrain of the mode is satisfied;

• ${\bf{f}}:{\cal Q} \to \left( {{\cal X} \to {{\mathbb{R}}^n}} \right)$ assigns to each $q \in {\cal Q}$ a locally Lipschitz continuous vector field ${{\bf{f}}_q}$ defined over ${\rm{Do}}{{\rm{m}}_q}$ ;

• ${\cal E} \subseteq {\cal Q} \times {\cal Q}$ is a set of edges (jumps);

• ${\cal G}:{\cal E} \to P\left( {\cal X} \right)$ assigns a guard condition ${{\cal G}_e}$ to each edge $e$ , s.t. the discrete jump can happen only if its guard is satisfied;

• ${\cal R}\left( { \cdot, \cdot } \right):{\cal E} \times {\cal X} \to P\left( {\cal X} \right)$ assigns a reset map ${{\cal R}_e}$ to each edge $e \in {\cal E}$ with ${{\cal R}_e}:{\cal X} \to P\left( {\cal X} \right)$ , that relates a state in the pre-mode to a set of states in the post-mode. ¹

The semantics of HA in terms of (hybrid) trajectories is defined in a standard way, please refer to (Zhan, Shuling, and Zhao 2017) for a comprehensive introduction to HA.

Now, we can formulate the problems of interest as follows.

Problem 1 (Reset Controller Synthesis) Given an HA ${\cal H}$ as Definition 1, we consider

• Problem 1.1: for a given safe set ${\cal S} \subseteq {\cal Q} \times {\cal X}$ , whether one can redefine $Init$ and ${\cal R}$ , and obtain a redesigned HA ${\cal H}{\rm{'}} = ({\cal Q},X,f,Ini{t^r},Dom,$ ${\cal E},{\cal G},{{\cal R}^r})$ , which is safe w.r.t. ${\cal S}$ .

• Problem 1.2: for a given safe set ${\cal S} \subseteq {\cal Q} \times {\cal X}$ and a target set $TR \subseteq {\cal Q} \times {\cal X}$ , whether one can redefine $Init$ and ${\cal R}$ , and obtain a redesigned HA ${\cal H}{\rm{'}} = ({\cal Q},X,f,Ini{t^r},Dom,$ ${\cal E},{\cal G},{{\cal R}^r})$ , s.t. for any $\left( {q,x} \right) \in Ini{t^r}$ , any trajectory starting from $\left( {q,x} \right)$ must reach ${\cal T}$ , and ${\cal H}{\rm{'}}$ is safe w.r.t. ${\cal S}$ before reaching into ${\cal T}$ .

To address the above two problems, the following notions are needed.

Definition 2 (Transverse Set) Given a vector field $f$ and a set $S \subseteq {{\mathbb{R}}^n}$ , the transverse set of $S$ w.r.t. $f$ , denoted by $tran{s_{f \uparrow S}}$ of $f$ over $S$ , is defined by

$${\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}\hat = \{ {\bf{x}} \in \partial S|\forall \varepsilon > 0,{\mkern 1mu} \,\exists t \in \left[ {0,\varepsilon } \right),\phi \left( {{\bf{x}},t} \right){\mkern 1mu} \notin {\mkern 1mu} S\} $$

where $\partial S$ is the boundary of $S$ .

Intuitively, any trajectory starting from the transverse set of $S$ w.r.t. ${\bf{f}}$ will leave $S$ immediately. For example, in Figure 2, ${{\bf{x}}_2} \in {\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}$ , ${{\bf{x}}_3} \in {\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}$ , ${{\bf{x}}_4} \in {\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}$ , but ${{\bf{x}}_1}\, \notin\, {\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}$ . Clearly, if ${\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}$ is empty, then any trajectory starting from $S$ stays within $S$ forever, which implies $S$ is a differential invariant (see Definition 3).

Figure 2. An example of transverse set. The arrows indicate the vector field of f. The area within the black square is a safe area $S$ . The dotted line on the lower border of the square indicates that this part of the boundary is not within the safe area.

Definition 3 (Differential Invariant (DI)) A set $C$ is a differential invariant of vector field $f$ w.r.t. a set $S$ if for all $x \in C$ and $T \ge 0$

$$\left( {\matrix{ {\forall t \in \left[ {0,T} \right].} \cr {\phi \left( {{\bf{x}},t} \right) \in S} \cr } } \right) \Rightarrow \left( {\matrix{ {\forall t \in \left[ {0,T} \right].} \cr {\phi \left( {{\bf{x}},t} \right) \in C} \cr } } \right)$$

In other words, ${\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S \cap C}} = \emptyset $ . Clearly, if $S \subseteq C$ , then $C$ is a DI of ${\bf{f}}$ w.r.t. $S$ . Normally, we are only interested in such DIs that are subsets of the domain constraint $S$ .

Definition 4 (Reach-Avoid Set) Given a vector field $f$ , an initial set ${{\cal X}_0}$ , a safe set ${\cal S}$ and a target set ${\cal T}$ , the (maximal) reach-avoid set $RA\left( {{X_0}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{\rm{f}}^S} T} \right)$ is defined by

$$\eqalign{ & {\rm{RA}}\left( {{{\cal X}_0}\mathop \to \limits_{\rm{f}}^S {\cal T}} \right)\widehat = \cr & \left\{ {{\bf{x}} \in {{\cal X}_0} \cap S\left| {{\rm{\;}}\matrix{ {} \hfill & {\exists T \ge 0,} \hfill \cr {} \hfill & {{\rm{\;\;\;\;}}\forall t \in \left[ {0,T} \right),\phi \left( {{\bf{x}},t} \right) \in S \wedge } \hfill \cr {} \hfill & {{\rm{\;\;\;\;}}\forall \varepsilon \gt 0,\exists t \in \left[ {T,T + \varepsilon } \right),\phi \left( {{\bf{x}},t} \right) \in {\cal T}} \hfill \cr } } \right.} \right\} \cr} $$

For example, in Figure 2, the blue shaded area (including the border) is ${\rm{RA}}( {{\cal S}\mathop \to \limits_{\rm{f}}^S {\rm{tran}}{{\rm{s}}_{{\bf{f}} \uparrow S}}})$ .

Problem 1.1 can be solved by requiring that in each mode $q \in {\cal Q}$ any continuous flow from the initial set ${\rm{Ini}}{{\rm{t}}_q}$ either

1. i) safely reaches the must-jump part of a jump eventually, that is ${ \cup _{p \in {\rm{Post}}\left( q \right)}}{\rm{RA}}({\rm{S}}{{\rm{D}}_q}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{f_q}}^{S{D_q}}} {\rm{Dom}}_q^c \cap {G_{e = \left( {q,p} \right)}}))$ , where ${\rm{S}}{{\rm{D}}_q} = {\rm{Do}}{{\rm{m}}_q} \cap {S_q}$ , ${\rm{Post}}\left( q \right)$ stands for the set of modes to which there is a jump from $q$ and ${\rm{Dom}}_q^c$ for the complement of ${\rm{Do}}{{\rm{m}}_q}$ ; or

2. ii) stays inside the mode forever and subject to the safety constraint, that is ${\rm{S}}{{\rm{D}}_q}\;\backslash \;{\rm{RA}}({\rm{S}}{{\rm{D}}_q}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{f_q}}^{S{D_q}}} {\rm{tran}}{{\rm{s}}_{{{\bf{f}}_q} \uparrow {\rm{S}}{{\rm{D}}_q}}})$ .

Obviously, i) corresponds to a reach-avoid problem, which considers how to compute the maximal set of initial states s.t. flows starting from them reach the target eventually while remaining inside the safe set before the reach. As showed in Liu et al. (2023), by introducing a template, whose 0-sublevel set is an inner-approximation of the reach-avoid set, the maximal reach-avoid set of polynomial hybrid automata can be inner-approximated by solving a certain convex programming problem, which can be done using off-the-shell SDP solvers. After that, new reset maps corresponding to the jump are also synthesized to guarantee safety in the post-mode. While, ii) corresponds to a differential invariant generation problem, which can be solved relatively well by exploiting existing methods (e.g., Liu, Zhan, and Zhao 2011; Ghorbal and Platzer 2014; Xue et al. 2019; Wang et al. 2022).

For example, consider a given HA and a safe set as in Figure 3. In the first step, we compute the must-jump parts respectively in ${q_1}$ and ${q_2}$ by computing the corresponding reach-avoid sets, and obtain

$${\rm{R}}{{\rm{A}}_1} = {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_1}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{f_{q1}}}^{S{D_{q1}}}} {\rm{tran}}{{\rm{s}}_{{{\bf{f}}_{{q_1}}} \uparrow {\rm{SD}}_{{q_1}}^c \cap {G_{{e_1}}}}}} \right),$$

$${\rm{R}}{{\rm{A}}_2} = {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_2}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{q2}}}^{S{D_{q2}}}} {\rm{tran}}{{\rm{s}}_{{{\bf{f}}_{{q_2}}} \uparrow {\rm{SD}}_{{q_2}}^c \cap {G_{{e_2}}}}}} \right)$$

Figure 3. An example for solving Problem 1.1. The areas enclosed by black squares represent the intersection of the domain and the safe set, denoted as ${\rm{S}}{{\rm{D}}_q}$ . The regions enclosed by orange circles indicate the initial sets, while those enclosed by blue circles represent the guard conditions. The red regions denote the differential invariants of the respective modes, while the green regions signify the reach-avoid sets.

In the second step, we can compute DIs respectively in ${q_1}$ and ${q_2}$ by computing the corresponding transverse set, and obtain

$$D{I_1} = {\rm{S}}{{\rm{D}}_{{q_1}}}\backslash {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_1}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{{q1}}}}}^{{\rm{S}}{{\rm{D}}_{{{q1}}}}}} {\rm{tran}}{{\rm{s}}_{{{\bf{f}}_{{q_1}}} \uparrow {\rm{S}}{{\rm{D}}_{{q_1}}}}}} \right),$$

$$D{I_2} = {\rm{S}}{{\rm{D}}_{{q_2}}}\backslash {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_2}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{{q2}}}}}^{{\rm{S}}{{\rm{D}}_{{\rm{q2}}}}}} {\rm{tran}}{{\rm{s}}_{{{\bf{f}}_{{q_2}}} \uparrow {\rm{S}}{{\rm{D}}_{{q_2}}}}}} \right)$$

Finally, we can redefine the initial set and reset map as follows:

$${\rm{Init}}_{{q_1}}^r = {\rm{Ini}}{{\rm{t}}_{{q_1}}} \cap \left( {{\rm{D}}{{\rm{I}}_1} \cup {\rm{R}}{{\rm{A}}_1}} \right),$$

$${\rm{Init}}_{{q_2}}^r = {\rm{Ini}}{{\rm{t}}_{{q_2}}} \cap \left( {{\rm{D}}{{\rm{I}}_2} \cup {\rm{R}}{{\rm{A}}_2}} \right),$$

$${\cal R}_{{e_1}}^r\left( x \right) \subseteq {\rm{D}}{{\rm{I}}_2} \cup {\rm{R}}{{\rm{A}}_2}\forall x \in {{\cal G}_{{e_1}}},$$

$${\cal R}_{{e_2}}^r\left( x \right) \subseteq {\rm{D}}{{\rm{I}}_1} \cup {\rm{R}}{{\rm{A}}_1}\forall x \in {{\cal G}_{{e_2}}}$$

The redefined HA is also shown in Figure 3.

Problem 1.2 In this case, step i) becomes more involved, as a flow may also reach the target set of the current mode, but it is still a reach-avoid problem and can thus be treated similarly. Furthermore, a non-trivial liveness constraint rules out the case of ii). However, an additional problem must be addressed, i.e., how to avoid the unreachability caused by infinite loops among the modes. This problem can be solved by searching and blocking all simple loops among the modes.

For example, to synthesize a reset controller for the HA given in Figure 4 with the given safe and target set, we have to

• block all trajectories that can reach ${q_3}$ , as ${{\cal T}_{{q_3}}} = \emptyset $ , which implies the liveness cannot be satisfied along these trajectories;

• block all trajectories with a simple loop containing ${q_0},{q_1}$ and ${q_2}$ , as such trajectories could evolve infinitely along the loop, and never reach the target.

Figure 4. An example of solving Problem 1.2.

We omit the technical details of how to implement the above idea by redefining the initial set and reset map, and technical details can be found in Liu et al. (2023).

Reset controller synthesis with time-delay

Time-delay is inevitable in the design of CPS, because of

• conversions between analog and digital signal domains,

• complex digital signal-processing chains enhancing,

• filtering and fusing sensory signals before they enter control,

• sensor networks harvesting multiple sensor sources before feeding them to control,

• network delays in networked control applications physically removing the controller(s) from the control path and just name a few.

The delay-free assumption makes the problem mathematically simple, but physically impossible, even impractical, as it may lead to deteriorated control performance and invalid verification certificates obtained by abstracting away time delay in practice. So, realistically, we should consider this issue in the context of time-delay like delay hybrid automata (Bai et al. 2021) so that the time spent by the reset controller can be modeled as time delay and thus it can be taken into account. Thus, we investigate the reset controller synthesis problem for delay hybrid systems (dHS), which contains delay in both continuous evolution and discrete transitions and propose a novel reach-avoid analysis based method.

Reach-avoid for delay differential equations (DDE)

Consider a DDE of the form

(1) $${\bf{\dot x}}\left( t \right) = {\bf{f}}\left( {{\bf{x}}\left( t \right),{\bf{x}}\left( {t - \tau } \right)} \right),{\rm{\;\;\;\;}}{\bf{f}} \in {\mathbb{R}}{\left[ {{\bf{x}}\left(t \right),{\bf{x}}\left( {t - \tau } \right)} \right]^n}$$

a safe set ${\cal S} \in {{\mathbb{R}}^n}$ and a target set ${\cal T} \in {{\mathbb{R}}^n}$ , a (the maximal) reach-avoid set ${\cal R}{\cal A}\left( {{\bf{f}},{\cal S},{\cal T}} \right)$ is defined as

$${\cal R}{\cal A}\left( {{\bf{f}},{\cal S},{\cal T}} \right)\widehat = \\ {\rm{\;}}\left\{ {\phi \in {\cal C}\left( {\left[ { - \tau, 0} \right],{\cal S}} \right)\left| {{\rm{\;}}\matrix{ {} \hfill & {\exists {\rm{\;}}t{\rm{'}} \in \mathbb{R},} \hfill \cr {} \hfill & {{\rm{\;\;\;\;}}{x^\phi }\left( {t{\rm{'}}} \right) \in T \wedge } \hfill \cr {} \hfill & {{\rm{\;\;\;\;}}\forall {\rm{\;}}t \in \left[ { - \tau, t{\rm{'}}} \right),{x^\phi }\left( t \right) \in {\cal S}} \hfill \cr } } \right.} \right\}$$

where ${\cal C}\left( {\left[ { - \tau, 0} \right],{\cal S}} \right)$ stands for the set of all continuous functions from $\left[ { - \tau, 0} \right]$ to ${\cal S}$ , ${x^\phi }$ denote the trajectory of (1) with initial function $\phi $ .

Definition 5 (Reach-Avoid Barrier Functional (RABFal)) Given a DDE of the form (1) with domain $D \subseteq {{\mathbb{R}}^n}$ , safe set ${\cal S}$ and target set ${\cal T}$ represented by

$${\cal S}\widehat = \{ {\bf{x}} \in D\,|\,s\left( {\bf{x}} \right) \le 0\}, $$

$${\cal T}\widehat = \{ {\bf{x}} \in D\,|\,g\left( {\bf{x}} \right) \le 0\} {\rm{\;}},$$

we call $H:{\cal C}\left( {\left[ { - \tau, 0} \right],D} \right) \to \mathbb{R}$ a reach-avoid barrier functional if we can find a bounded function $w:D \to \mathbb{R}$ such that the following conditions are satisfied:

(2) $$ - {{dH\left( {{{\bf{x}}_t}} \right)} \over {dt}} \ge 0,\forall \;{{\bf{x}}_t} \in C\left( {\left[ { - \tau, 0} \right],{\cal S}} \right)$$

(3) $$H\left( {{{\bf{x}}_t}} \right) \ge 0,\forall {\rm{\;}}{{\bf{x}}_t} \in {\cal C}\left( {\left[ { - \tau, 0} \right],{\cal S}} \right),\,s.t.\ {{\bf{x}}_t}\left( 0 \right) \in \partial {\cal S}$$

(4) $$H\left( {{{\bf{x}}_t}} \right) - {{dw\left( {{{\bf{x}}_t}\left( 0 \right)} \right)} \over {dt}} \ge g\left( {{{\bf{x}}_t}\left( 0 \right)} \right),\forall \;{{\bf{x}}_t} \in C\left( {\left[ { - \tau, 0} \right],{\cal S}} \right)$$

Theorem 1 (Su et al. 2023) Given a DDE of the form (1), safe set ${\cal S}$ and target set ${\cal T}$ , the set ${\cal R}{{\cal A}_{in}}$ defined by the 0-sublevel set of $H$ , i.e.,

(5) $${\cal R}{{\cal A}_{in}}\widehat = \{ \phi \in {\cal C}\left( {\left[ { - \tau, 0} \right],{\cal S}} \right)|H\left( \phi \right) \lt 0\} $$

is an inner-approximation of ${\cal R}{\cal A}\left( {{\bf{f}},{\cal S},{\cal T}} \right)$ , i.e., ${\cal R}{{\cal A}_{in}} \subseteq {\cal R}{\cal A}\left( {{\bf{f}},Safe,{\cal T}} \right)$ .

In Su et al. (2023), it is proved that synthesizing such RABFal can be reduced to solving SDP.

Definition 6 (Delay Hybrid Automata (dHA) (Bai et al. 2021 )) A dHA ${\cal H}$ is a tuple $\left( {{\cal Q},X,Init,Dom,f,{\cal E},{\cal G},{\cal R},ST} \right)$ , where

• ${\cal Q} = \left\{ {{q_1}, \ldots, {q_m}} \right\}$ is a finite set of modes;

• $X = \left\{ {{x_1}, \ldots, {x_n}} \right\}$ is a set of continuous state; variables, written as ${\bf{x}} = \left( {{x_1}, \ldots, {x_n}} \right) \in {{\mathbb{R}}^n}$ ;

• ${\rm{Init}} \subseteq {\cal Q} \times {\cal C}\left( {\left[ { - \tau, 0} \right],{{\mathbb{R}}^n}} \right)$ assigns a set of initial states to each mode;

• ${\rm{Dom}}:{\cal Q} \to {2^{{{\mathbb{R}}^n}}}$ defines a domain constraint for each mode $q \in {\cal Q}$ , denoted by ${\rm{Do}}{{\rm{m}}_q} \subseteq {{\mathbb{R}}^n}$

• ${\bf{f}}:{\cal Q} \to \left( {{\cal C}\left( {\left[ { - \tau, 0} \right],{{\mathbb{R}}^n}} \right) \to {{\mathbb{R}}^n}} \right)$ defines the continuous dynamics with delay for each mode $q$ , denoted by ${{\bf{f}}_q}$ with the type ${\cal C}\left( {\left[ { - \tau, 0} \right],{{\mathbb{R}}^n}} \right) \to {{\mathbb{R}}^n}$ ;

• ${\cal E} \subseteq {\cal Q} \times {\cal Q}$ is a set of discrete transitions;

• ${\cal G}:{\cal E} \to {2^{{{\mathbb{R}}^n}}}$ assigns a switching guard ${{\cal G}_e}$ $ \subseteq {{\mathbb{R}}^n}$ to each discrete transition $e \in {\cal E}$ ;

• ${\cal R}:{\cal E} \to \left( {{{\mathbb{R}}^n} \to {\cal C}\left( {\left[ { - \tau, 0} \right],{{\mathbb{R}}^n}} \right)} \right)$ assigns a reset function ${{\cal R}_e}$ to each discrete transition $e \in {\cal E}$ with ${{\cal R}_e}:{{\mathbb{R}}^n} \to {\cal C}\left( {\left[ { - \tau, 0} \right],{{\mathbb{R}}^n}} \right)$ ;

• $ST \subseteq {\cal E} \times \mathbb{R}$ assigns a switching time to each discrete transition $e \in {\cal E}$ .

Problem 2 (Reset Controller Synthesis for dHA) Given a dHA ${\cal H}$ as Definition 6, for a given compact safe set ${\cal S} \subseteq Q \times X$ and a compact target set ${\cal T} \subseteq Q \times X$ , whether we can find a new $Ini{t^r}$ and ${{\cal R}^r}$ such that all executions of the redesigned dHA ${{\cal H}^r} = \left( {{\cal Q},X,Init,Dom,f,{\cal E},{\cal G},{{\cal R}^r},Ini{t^r},ST} \right)$ will reach ${\cal T}$ while stay in ${\cal S}$ before that.

With the above notions and notations, Problem 2 can be solved quite similarly to Problem 1.2, we will use the following example to illustrate the procedure, the details can be found in Su et al. (2023).

As an illustrative example, consider a dHA given by Figure 5. The synthesis procedure can be sketched by the following four steps:

Figure 5. A running example of dHA.

Step 1: First, compute the reach-avoid set for each mode w.r.t. the target and the guards of the outgoing jumps from it and then partition a mode into several sub-modes so that their reach-avoid sets are mutually disjoint. For instance, for the running example, as shown in Figure 6, ${q_1}$ is split into three sub-modes ${q_{11}},{q_{12}}$ and ${q_{13}}$ , their reach-avoid sets are computed as below:

$$R{A_{in}}\left( {1,1} \right)\,\widehat =\, {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_1}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{\rm{q1}}}}}^{{\rm{S}}{{\rm{D}}_{{{q1}}}}}} {g_{11}} \cap {\rm{Dom}}_{{q_1}}^c} \right)$$

$$R{A_{in}}\left( {1,2} \right)\,\widehat =\, {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_1}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{{q1}}}}}^{{\rm{S}}{{\rm{D}}_{{{q1}}}}}} {g_{12}} \cap {\rm{Dom}}_{{q_1}}^c} \right)$$

$$R{A_{in}}\left( {1,3} \right)\,\widehat =\, {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_1}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{{q1}}}}}^{{\rm{S}}{{\rm{D}}_{{{q1}}}}}} {g_{13}} \cap {\rm{Dom}}_{{q_1}}^c} \right)$$

Figure 6. Mode partition of ${q_1}$ . On the left side, we have mode ${q_1}$ with guard conditions ${\cal G}\left( {{e_1}} \right)$ and ${\cal G}\left( {{e_2}} \right)$ represented by blue slashes, and their intersection is depicted by orange slashes. The reach-avoid set to ${\cal G}\left( {{e_1}} \right) \cup {\cal G}\left( {{e_2}} \right)$ 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}}$ .

With the same manner, the partition of mode ${q_3}$ is shown in Figure 7. Their reach-avoid set are computed as below:

$$R{A_{in}}\left( {3,0} \right)\,\widehat =\, {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_3}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{{q3}}}}}^{{\rm{S}}{{\rm{D}}_{{{q3}}}}}} {g_{30}}} \right)$$

$$R{A_{in}}\left( {3,1} \right)\,\widehat =\, {\rm{RA}}\left( {{\rm{S}}{{\rm{D}}_{{q_3}}}\mathrel{\mathop{\kern0pt\longrightarrow}\limits_{{{\rm{f}}_{{q_3}}}}^{{\rm{S}}{{\rm{D}}_{{q_3}}}}} {g_{31}} \cap {\rm{Dom}}_{{q_3}}^c} \right)$$

Second, introduce necessary jumps between these sub-modes. Let’s consider ${q_{31}}$ in the running example, edges from ${q_{31}}$ to the sub-modes of ${q_1}$ are introduced, i.e., including $\left( {{q_{31}},{q_{11}}} \right),\left( {{q_{31}},{q_{12}}} \right)$ and $\left( {{q_{31}},{q_{13}}} \right)$ .

Figure 7. Mode partition of ${q_3}$ . The left side is mode ${q_3}$ with the guard condition ${{\cal G}_{{e_3}}}$ (blue slashes) and the target set ${{\cal T}_{{q_3}}}$ (green slashes). Correspondingly, ${q_3}$ is partitioned into two sub-modes: ${q_{30}}$ with ${g_{30}} = {{\cal T}_{{q_3}}}$ and ${q_{31}}$ with ${g_{31}} = {{\cal G}_{{e_3}}}$ .

Third, define a reset map for each introduced edge. Continue the above example, we have

$${\cal R}_{\left( {{q_{31}},{q_{11}}} \right)}^m\left( {\bf{x}} \right) \subseteq {\cal R}{{\cal A}_{in}}\left( {1,1} \right),\forall {\bf{x}} \in {g_{31}}$$

$${\cal R}_{\left( {{q_{31}},{q_{12}}} \right)}^m\left( {\bf{x}} \right) \subseteq {\cal R}{{\cal A}_{in}}\left( {1,2} \right),\forall {\bf{x}} \in {g_{31}}$$

$${\cal R}_{\left( {{q_{31}},{q_{13}}} \right)}^m\left( {\bf{x}} \right) \subseteq {\cal R}{{\cal A}_{in}}\left( {1,3} \right),\forall {\bf{x}} \in {g_{31}}$$

$${\cal R}_{\left( {{q_{13}},{q_{30}}} \right)}^m\left( {\bf{x}} \right) \subseteq {\cal R}{{\cal A}_{in}}\left( {3,0} \right),\forall {\bf{x}} \in {g_{13}}$$

$${\cal R}_{\left( {{q_{13}},{q_{31}}} \right)}^m\left( {\bf{x}} \right) \subseteq {\cal R}{{\cal A}_{in}}\left( {3,1} \right),\forall {\bf{x}} \in {g_{13}}$$

$$ \cdots $$

Step 2: Abstract away continuous dynamics in each resulted mode and obtain a discrete-directed graph (DDG). For the running example, it results a DDG given in Figure 8.

Figure 8. The resulting discrete-directed graph.

Step 3: Prune unsatisfied paths in the DDG, which are either unreachable like $\langle {q_{14}},{q_2}\rangle $ and $\langle {q_{31}},{q_{12}},{q_2}\rangle $ or simple loops like $\langle {q_{14}},{q_{31}},{q_{14}}\rangle $ . The DDG after pruning is depicted in Figure 9, where only two edges ( ${e_{11}},{e_{12}}$ ) are left.

Figure 9. The discrete directed graph after edges prunning.

Step 4: Synthesize a reset controller from the resulted DDG. Continue the running example, we obtain

$${\cal R}_{{e_2}}^r\left( x \right) = R_{{e_{12}}}^m\left( {\bf{x}} \right),\forall x \in {\cal G}_{{e_{12}}}^m = {{\cal G}_{{e_2}}}\backslash {{\cal G}_{{e_1}}}$$

$${\cal R}_{{e_2}}^r\left( x \right) = R_{{e_{11}}}^m\left( {\bf{x}} \right),\forall x \in {\cal G}_{{e_{11}}}^m = {{\cal G}_{{e_2}}} \cap {{\cal G}_{{e_1}}}$$

$${\rm{Init}}_{{q_1}}^r = {\rm{Init}}_{{q_{12}}}^m \cup {\rm{Init}}_{{q_{13}}}^m.$$

Conclusion

In summary, we sketched our recent work on reset controller synthesis, including

• how to reduce the problem of synthesizing reset controllers w.r.t. safety and liveness constraints to reach-avoid set computation and differential invariant generation problems;

• how to inner-approximate reach-avoid sets by solving certain convex programming problems, which can be efficiently conducted using off-the-shell SDP solvers;

• how to synthesize reset controller for dHSs by reducing it into reach-avoid analysis for DDE and depth-first-search with block for discrete-event dynamics.

Regarding future work, we emphasize the following topics along this research line:

• To extend our approach to more general hybrid systems with more complicated vector fields, e.g., probabilistic and stochastic behavior, the combination of time-delay and stochasticity and so on.

• To investigate potential correct-by-construction frameworks for HSs by taking feedback controller synthesis, switching logic controller synthesis and reset controller synthesis into account uniformly.

• To integrate recent advances on differential invariant generation by reduction non-convex programming to SDP, e.g., in Wang et al. (2021, 2022) into our synthesis framework.

• To conduct more complicated and practical case studies.