Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-23T03:24:59.284Z Has data issue: false hasContentIssue false

Reset controller synthesis: a correct-by-construction way to the design of CPS

Published online by Cambridge University Press:  18 October 2024

A response to the following question: What are the fundamental software abstractions for designing reliable cyber-physical systems operating in uncertain environments?

Naijun Zhan
Affiliation:
School of Computer Science, Peking University, Beijing, China SKLCS, Institute of Software, CAS, Beijing, China University of Chinese Academy of Sciences, CAS, Beijing, China
Han Su
Affiliation:
SKLCS, Institute of Software, CAS, Beijing, China University of Chinese Academy of Sciences, CAS, Beijing, China
Mengfei Yang
Affiliation:
China Academy of Space Technology, Beijing, China
Bin Gu*
Affiliation:
Beijing Institute of Control Engineering, Beijing, China
*
Corresponding author: Bin Gu; Email: [email protected]
Rights & Permissions [Opens in a new window]

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.

Type
Results
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.
Copyright
© The Author(s), 2024. Published by Cambridge University Press

Introduction

As defined by Baheti and Gill (Reference Baheti and Gill2011), 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. Reference Tomlin, Lygeros and Sastry2000; Asarin et al. Reference Asarin, Bournez, Dang, Maler and Pnueli2000; Coogan and Arcak Reference Coogan and Arcak2012; Jha et al. Reference Jha, Gulwani, Seshia and Tiwari2010; Taly, Gulwani, and Tiwari Reference Taly, Gulwani and Tiwari2011; Girard Reference Girard2012; Gulwani and Tiwari Reference Gulwani and Tiwari2008; Taly, Gulwani, and Tiwari Reference Taly, Gulwani and Tiwari2011; Zhao, Zhan, and Kapur Reference Zhao, Zhan and Kapur2013) 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. Reference Brentari, Urbina, Arzelier, Louembet and Zaccarian2018), 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. Reference Liu, Su, Bai, Gu, Xue, Yang and Zhan2023)). 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. Reference Frehse, Le Guernic, Donzé, Cotton, Ray, Lebeltel, Ripado, Girard, Dang and Maler2011), iSAT-ODE (Eggers, Fränzle, and Herde Reference Eggers, Fränzle and Herde2008), dReach (Kong et al. Reference Kong, Gao, Chen and Clarke2015) and Flow* (Chen, Ábrahám, and Sankaranarayanan Reference Chen, Ábrahám and Sankaranarayanan2013) 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 Reference Platzer2012) and hyrid Hoare logic (HHL) (Liu et al. Reference Liu, Lv, Quan, Zhan, Zhao, Zhou and Zou2010; Zhan et al. Reference Zhan, Zhan, Wang, Guelev and Jin2023). dL demonstrates significant capability in deducing verification for HSs, proving effective across various verification challenges, including the verification of liveness properties (Tan and Platzer Reference Tan and Platzer2019) and switched systems (Tan and Platzer Reference Tan and Platzer2021) with the help of the tool KeYmaera X (Platzer Reference Platzer2010). 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 Reference Wang, Zhan and Zou2015). Event-B (Richard Reference Richard2024; Richard et al. Reference Richard, Michael, Qin and Zhu2017; Richard et al. Reference Richard, Michael, Qin, Verma and Zhu2015; Butler, Abrial, and Banach Reference Butler, Abrial and Banach2016; Dupont et al. Reference Dupont, Ait-Ameur, Kumar Singh and Pantel2021; Dupont et al. Reference Dupont, Aı¨t-Ameur, Kumar Singh and Pan-tel2022) 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 Reference Back and Wright2012) or controller synthesis semantically (Bozga and Sifakis Reference Bozga and Sifakis2022). 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 (Reference Loos and Platzer2016) proposed differential refinement logic to cope with refinement relation among different levels of abstraction for a given HS. Yan et al. (Reference Yan, Jiao, Wang, Wang and Zhan2020) defined a set of refinement rules for transforming HCSP to System C, and Wang et al. (Reference Wang, Ji, Xu, Zhan, Gao and Zhan2024) 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 Reference Zhao, Mohan and Vasudevan2019), Hamilton-Jacobi-based methods (Tomlin, Lygeros, and Sastry Reference Tomlin, Lygeros and Sastry2000), barrier certificates-based methods (Ames et al. Reference Ames, Xu, Grizzle and Tabuada2016), abstraction-based methods (Girard Reference Girard2012), and counter-example-guided inductive synthesis methods (Abate et al. Reference Abate, Bessa, Do, Cordeiro, David, Kesseli, Kroening and Polgreen2017). Another category addresses the synthesis problem of switching controllers, which can be classified into abstraction-based methods (Girard Reference Girard2012; Tabuada Reference Tabuada2009; Belta, Yordanov, and Gol Reference Belta, Yordanov and Aydin Gol2017) and constraint-solvingbased methods (Taly, Gulwani, and Tiwari Reference Taly, Gulwani and Tiwari2011; Zhao, Zhan, and Kapur Reference Zhao, Zhan and Kapur2013; Taly and Tiwari Reference Taly and Tiwari2010). However, since its initial exploration in Clegg (Reference Clegg1958), 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. (Reference Liu, Su, Bai, Gu, Xue, Yang and Zhan2023) and Su et al. (Reference Su, Zhu, Feng, Bai, Gu, Liu, Yang and Zhan2023).

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.Footnote 1

The semantics of HA in terms of (hybrid) trajectories is defined in a standard way, please refer to (Zhan, Shuling, and Zhao Reference Zhan, Shuling and Zhao2017) 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. (Reference Liu, Su, Bai, Gu, Xue, Yang and Zhan2023), 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 Reference Liu, Zhan and Zhao2011; Ghorbal and Platzer Reference Ghorbal and Platzer2014; Xue et al. Reference Xue, Wang, Zhan and Fränzle2019; Wang et al. Reference Wang, Chen, Xue, Zhan and Katoen2022).

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. (Reference Liu, Su, Bai, Gu, Xue, Yang and Zhan2023).

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. Reference Bai, Gan, Jiao, Xia, Xue and Zhan2021) 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. Reference Su, Zhu, Feng, Bai, Gu, Liu, Yang and Zhan2023) 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. (Reference Su, Zhu, Feng, Bai, Gu, Liu, Yang and Zhan2023), it is proved that synthesizing such RABFal can be reduced to solving SDP.

Definition 6 (Delay Hybrid Automata (dHA) (Bai et al. Reference Bai, Gan, Jiao, Xia, Xue and Zhan2021 )) 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. (Reference Su, Zhu, Feng, Bai, Gu, Liu, Yang and Zhan2023).

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. (Reference Wang, Chen, Xue, Zhan and Katoen2021, Reference Wang, Chen, Xue, Zhan and Katoen2022) into our synthesis framework.

  • To conduct more complicated and practical case studies.

Code & data availability statement

All code can be found in GitHub: https://github.com/Han-SU/Reset-Controller-Synthesis.git.

Acknowledgements

I would like to thank all collaborators involved in this research, including Jiang Liu, Yunjun Bai, Bai Xue, Jiyu Zhu, etc.

Author contribution

Naijun Zhan, Mengfei Yang and Bin Gu contributed the theoretical part, and Han Su contributed the experimental part of this paper.

Funding statement

This work was partly funded by the NSFC under grant no. 62192730&62192732&62192735 and the CAS Project for Young Scientists in Basic Research under grant no. YSBR-040.

Competing interests

None.

Ethics statement

Ethical approval was obtained from the Ethics Committee of Peking University and University of Chinese Academy of Sciences. Study participants gave written informed consent to take part in the study.

Footnotes

1 For an edge $e = \left( {q,p} \right)$ , we refer to $q$ as the pre-mode of $e$ , and $p$ as the post-mode of $e$

References

Connections references

Broman, D and Woodcock, J (2023) What are the fundamental software abstractions for designing reliable cyber-physical systems operating in uncertain environments? Research Directions: Cyber-Physical Systems 1, e4. https://doi.org/10.1017/cbp.2023.4 Google Scholar

References

Abate, A, Bessa, I, Do, C, Cordeiro, L, David, C, Kesseli, P, Kroening, D, and Polgreen, E. (2017) Automated formal synthesis of digital controllers for state-space physical plants. In CAV’17. Springer, pp. 462482.Google Scholar
Ames, A, Xu, X, Grizzle, JW, and Tabuada, P (2016) Control barrier function based quadratic programs for safety critical systems. IEEE Transactions on Automatic Control 62(8), 38613876.Google Scholar
Asarin, E, Bournez, O, Dang, T, Maler, O, and Pnueli, A. (2000) Effective synthesis of switching controllers for linear systems. Proceedings of the IEEE 88(7), 10111025.Google Scholar
Back, R-J, and Wright, J. (2012) Refinement Calculus: A Systematic Introduction. Springer Science & Business Media.Google Scholar
Baheti, R, and Gill, H (2011) Cyber-physical systems. The Impact of Control Technology 12(1), 161166.Google Scholar
Bai, Y, Gan, T, Jiao, L, Xia, B, Xue, B, and Zhan, N (2021) Switching controller synthesis for delay hybrid systems under perturbations. In HSCC’21, pp. 111.Google Scholar
Belta, C, Yordanov, B, and Aydin Gol, E (2017) Formal Methods for Discrete-time Dynamical Systems. Vol. 89. Springer.Google Scholar
Bozga, M, and Sifakis, J (2022) Correct by design coordination of autonomous driving systems. In ISoLA’22. Springer, pp. 1329.Google Scholar
Brentari, M, Urbina, S, Arzelier, D, Louembet, C, and Zaccarian, L (2018) A hybrid control framework for impulsive control of satellite rendezvous. IEEE Transactions on Control Systems Technology 27(4), 15371551.Google Scholar
Butler, MJ, Abrial, J-R, and Banach, R (2016) Modelling and Refining Hybrid Systems in Event-b and Rodin.Google Scholar
Chen, X, Ábrahám, E, and Sankaranarayanan, S (2013) Flow*: an analyzer for non-linear hybrid systems. In CAV’13. Springer, pp. 258263.Google Scholar
Clegg, JC (1958) A nonlinear integrator for servomechanisms. Transactions of the American Institute of Electrical Engineers, Part II: Applications and Industry 77(1), 4142.Google Scholar
Coogan, S, and Arcak, M (2012) Guard synthesis for safety of hybrid systems using sum of squares programming. In CDC’12. IEEE, pp. 61386143.Google Scholar
Dupont, G, Ait-Ameur, Y, Kumar Singh, N, and Pantel, M (2021) Event-B hybridation: a proof and refinement-based frame- work for modelling hybrid systems. ACM Transactions on Embedded Computing Systems 20(4), 137.Google Scholar
Dupont, G, Aı¨t-Ameur, Y, Kumar Singh, N, and Pan-tel, M (2022) Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B. Science of Computer Programming 216, 102765.Google Scholar
Eggers, A, Fränzle, M, and Herde, C (2008) SAT modulo ODE: a direct SAT approach to hybrid systems. In ATVA’08. Springer, pp. 171185.Google Scholar
Frehse, G, Le Guernic, C, Donzé, A, Cotton, S, Ray, R, Lebeltel, O, Ripado, R, Girard, A, Dang, T, and Maler, O (2011) SpaceEx: Scalable verification of hybrid systems. In CAV’11. Springer, pp. 379395.Google Scholar
Ghorbal, K, and Platzer, A (2014) Characterizing algebraic invariants by differential radical invariants. In TACAS’14. Springer, pp. 279294.Google Scholar
Girard, A (2012) Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947953.Google Scholar
Gulwani, S, and Tiwari, A (2008) Constraint-based approach for analysis of hybrid systems. In CAV’08’. Springer, pp. 190203.Google Scholar
Jha, S, Gulwani, S, Seshia, SA, and Tiwari, A (2010) Synthesizing switching logic for safety and dwell-time requirements. In ICCPS’10, pp. 2231.Google Scholar
Kong, S, Gao, S, Chen, W, and Clarke, E (2015) Dreach: δ-reachability analysis for hybrid systems. In TACAS’15. Springer, pp. 200205.Google Scholar
Liu, J, Lv, J, Quan, Z, Zhan, N, Zhao, H, Zhou, C, and Zou, L (2010) A calculus for hybrid csp. In ASPLS’10. Springer, pp. 115.Google Scholar
Liu, J, Su, H, Bai, Y, Gu, B, Xue, B, Yang, M, and Zhan, N (2023) Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller. arXiv: 2309.05906 [eess.SY].Google Scholar
Liu, J, Zhan, N, and Zhao, H (2011) Computing semi-algebraic invariants for polynomial dynamical systems. In EMSOFT’11, pp. 97106.Google Scholar
Loos, SM, and Platzer, A (2016) Differential refinement logic. In LICS’16, pp. 505514.Google Scholar
Platzer, A (2010) Differential-algebraic dynamic logic for differential- algebraic programs. Journal of Logic and Computation 20(1), 309352.Google Scholar
Platzer, A (2012) Logics of dynamical systems. In LICS’12. IEEE, pp. 1324.Google Scholar
Richard, B (2024) Core hybrid Event-B III: fundamentals of a reasoning framework. Science of Computer Programming 231, 103002.Google Scholar
Richard, B, Michael, B, Qin, S, Verma, N, and Zhu, H (2015) Core hybrid Event-B I: single hybrid Event-B machines. Science of Computer Programming 105, 92123.Google Scholar
Richard, B, Michael, B, Qin, S, and Zhu, H (2017) Core hybrid Event-B II: multiple cooperating hybrid Event-B machines. Science of Computer Programming 139, 135.Google Scholar
Su, H, Zhu, J, Feng, S, Bai, Y, Gu, B, Liu, J, Yang, M, and Zhan, N (2023) Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems. arXiv: 2309.05908 [eess.SY].Google Scholar
Tabuada, P (2009) Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media.Google Scholar
Taly, A, Gulwani, S, and Tiwari, A. (2011) Synthesizing switching logic using constraint solving. International Journal on Software Tools for Technology Transfer 13(6), 519535.Google Scholar
Taly, A, and Tiwari, A. (2010) Switching logic synthesis for reachability. In EMSOFT’10, pp. 1928.Google Scholar
Tan, YK and Platzer, A (2019) An axiomatic approach to liveness for differential equations. In FM’19. Springer, pp. 371388.Google Scholar
Tan, YK and Platzer, A (2021) Switched systems as hybrid programs. IFAC-PapersOnLine 54(5), 247252.Google Scholar
Tomlin, CJ, Lygeros, J, and Sastry, SS. 2000. A game theoretic approach to controller design for hybrid systems. Proceedings of the IEEE 88(7), 949970.Google Scholar
Wang, Q, Chen, M, Xue, B, Zhan, N, and Katoen, J-P (2021) Synthesizing invariant barrier certificates via difference- of-convex programming. In CAV’21. Springer, pp. 443466.Google Scholar
Wang, Q, Chen, M, Xue, B, Zhan, N, and Katoen, J-P (2022) Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming. Information and Computer Science 289(Part), 104965.Google Scholar
Wang, S, Ji, Z, Xu, X, Zhan, B, Gao, Q, and Zhan, N (2024) Formally verified c code generation from hybrid commu- nicating sequential processes. In ICCPS’24. IEEE, pp. 123134.Google Scholar
Wang, S, Zhan, N, and Zou, L (2015) An improved HHL prover: an interactive theorem prover for hybrid systems. In ICFEM’15. Springer, pp. 382399.Google Scholar
Xue, B, Wang, Q, Zhan, N, and Fränzle, M (2019) Robust invariant sets generation for state-constrained perturbed polynomial systems. In HSCC’19, pp. 128137.Google Scholar
Yan, G, Jiao, L, Wang, S, Wang, L, and Zhan, N (2020) Automatically generating SystemC code from HCSP formal models. ACM Transactions on Software Engineering and Methodology 29(1), 139.Google Scholar
Zhan, N, Shuling, W, and Zhao, H (2017) Formal Verification of Simulink/Stateflow Diagrams: A Deductive Approach. Cham: Springer.Google Scholar
Zhan, N, Zhan, B, Wang, S, Guelev, D, and Jin, X (2023) A generalized hybrid Hoare logic. arXiv: 2303.15020 [cs.LO].Google Scholar
Zhao, H, Zhan, N, and Kapur, D (2013) Synthesizing switching controllers for hybrid systems by generating invariants. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng he on the Occasion of His 70th Birthday, 8051, LNCS, pp. 354373.Google Scholar
Zhao, P, Mohan, S, and Vasudevan, R (2019) Optimal control of polynomial hybrid systems via convex relaxations. IEEE Transactions on Automatic Control 65(5), 20622077.Google Scholar
Figure 0

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

Figure 1

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.

Figure 2

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.

Figure 3

Figure 4. An example of solving Problem 1.2.

Figure 4

Figure 5. A running example of dHA.

Figure 5

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}}$.

Figure 6

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}}}$.

Figure 7

Figure 8. The resulting discrete-directed graph.

Figure 8

Figure 9. The discrete directed graph after edges prunning.

Author comment: Reset Controller Synthesis: A Correct-by-Construction Way to the Design of CPS — R0/PR1

Comments

No accompanying comment.

Decision: Reset Controller Synthesis: A Correct-by-Construction Way to the Design of CPS — R0/PR2

Presentation

Overall score 4 out of 5
Is the article written in clear and proper English? (30%)
5 out of 5
Is the data presented in the most useful manner? (40%)
5 out of 5
Does the paper cite relevant and related articles appropriately? (30%)
3 out of 5

Context

Overall score 4 out of 5
Does the title suitably represent the article? (25%)
3 out of 5
Does the abstract correctly embody the content of the article? (25%)
5 out of 5
Does the introduction give appropriate context and indicate the relevance of the results to the question or hypothesis under consideration? (25%)
5 out of 5
Is the objective of the experiment clearly defined? (25%)
5 out of 5

Results

Overall score 4 out of 5
Is sufficient detail provided to allow replication of the study? (50%)
4 out of 5
Are the limitations of the experiment as well as the contributions of the results clearly outlined? (50%)
4 out of 5

Author comment: Reset Controller Synthesis: A Correct-by-Construction Way to the Design of CPS — R1/PR3

Comments

No accompanying comment.

Decision: Reset Controller Synthesis: A Correct-by-Construction Way to the Design of CPS — R1/PR4

Comments

No accompanying comment.