Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations

Abstract

Delays in feedback control loop, as induced by networked distributed control schemes, may have detrimental effects on control performance. This induces an interest in safety verification of delay differential equations (DDEs) used as a model of embedded control. This article explores reachable-set computation for a class of DDEs featuring a local homeomorphism property. This topological property facilitates construction of over- and under-approximations of their full reachable sets by performing reachability analysis on the boundaries of their initial sets, thereby permitting an efficient lifting of reach-set computation methods for ODEs to DDEs. Membership in this class of DDEs is determined by conducting sensitivity analysis of the solution mapping with respect to the initial states to impose a bound constraint on the time-lag term. We then generalize boundary-based reachability analysis to such DDEs. Our reachability algorithm is iterative along the time axis and the computations in each iteration are performed in two steps. The first step computes an enclosure of the set of states reachable from the boundary of the step’s initial state set. The second step derives an over- and under-approximations of the full reachable set by including (excluding, resp.) the obtained boundary enclosure from certain convex combinations of points in that boundary enclosure. Experiments on two illustrative examples demonstrate the efficacy of our algorithm.

Appendix

The Proof of Lemma 1

Proof

From Eq. (6), we obtain that

$$s^{ij}_{\varvec{x}_0}(t)=\varvec{I}^{ij}+\varvec{J}^{ij}t,$$

where $\varvec{J}^{ij}=\Big (D_{\varvec{g}}(\varvec{\phi }(t;\varvec{x}_0))s_{\varvec{x}_0}(t)\Big )_{t=\tau _{ij}}^{ij}$, $\tau _{ij}$ lies between 0 and t, $\varvec{s}_{\varvec{x}_0}^{ij}$ is the $(i,j)_{th}$ element of the matrix $\varvec{s}_{\varvec{x}_0}$ and $\varvec{J}^{ij}$ is the $(i,j)_{th}$ element of the matrix $D_{\varvec{g}}(\varvec{\phi }(t;\varvec{x}_0))s_{\varvec{x}_0}(t)$ with $t=\tau _{ij}$. Also, since $\varvec{g}(\varvec{x})\in \mathcal {C}^1(\mathcal {X})$, i.e. $\varvec{g}(\cdot ): \mathcal {X}\mapsto \mathbb {R}^n$ is a continuously differentiable function, the element in the matrix $D_{\varvec{g}}=\frac{\partial \varvec{g}}{\partial \varvec{x}}$ is bounded over an arbitrary compact set covering the reachable set $\cup _{t\in [0,\tau _1]}\varOmega (t;\mathcal {I}_0)$ in the set $\mathcal {X}$, where $\tau _1$ can be any number in $(0,\tau ]$ such that $\cup _{t\in [0,\tau _1]}\varOmega (t;\mathcal {I}_0)\subseteq \mathcal {X}$. The bounded property also applies to the matrix $s_{\varvec{x}_0}(t)$. Consequently, a lower bound for all elements of the matrix $\varvec{J}$ exists. Thus, $lim_{t\rightarrow 0}s_{\varvec{x}_0}(t)=\varvec{I}$ implies that there exists a $\tau ^{*}\in (0,\tau _1]$ s.t. the sensitivity matrix $s_{\varvec{x}_0}(t)$ for $t\in [0,\tau ^{*}]$ is diagonally dominant. The conclusion follows from this fact.    $\square$

The Proof of Lemma 2

Proof

Since the determinant of the Jacobian matrix of the mapping $\varvec{x}(t)=\varvec{\psi }_{k-1}(t;\varvec{x}((k-1)\tau ,(k-1)\tau )$ w.r.t. any state $\varvec{x}((k-1)\tau ) \in \varOmega ((k-1)\tau ;\mathcal {I}_0)$ is not zero for $t\in [(k-1)\tau ,k\tau ]$, then for any fixed $t\in [(k-1)\tau ,k\tau ]$, the mapping

$$\varvec{x}(t)=\varvec{\psi }_{k-1}(t;\ \cdot ,(k-1)\tau ): \varOmega ((k-1)\tau ;\mathcal {I}_0)\longmapsto \varOmega (t;\mathcal {I}_0)$$

is a bijection and its inverse mapping from $\varOmega (t;\mathcal {I}_0)$ to $\varOmega ((k-1)\tau ;\mathcal {I}_0)$ is continuously differentiable. Thus, the sensitivity matrix $s_{\varvec{x}(k\tau )}(t)$ for $t\in [k\tau ,(k+1)\tau ]$ satisfies the sensitivity equation:

$$\dot{s}_{\varvec{x}(k\tau )}=\frac{\partial \varvec{f}(\varvec{x},\varvec{x}_{\tau })}{\partial \varvec{x}}s_{\varvec{x}(k\tau )}+\frac{\partial \varvec{f}(\varvec{x},\varvec{x}_{\tau })}{\partial \varvec{x}_{\tau }}\frac{\partial \varvec{x}_{\tau }}{\partial \varvec{x}(k\tau )},$$

with $s_{\varvec{x}(k\tau )}(k\tau )=\varvec{I}\in \mathbb {R}^{n\times n}$.    $\square$