Taming Delays in Dynamical Systems

Abstract

Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it consequently is omnipresent in safety-critical domains, there is an increasing interest in the safety verification of systems modelled by Delay Differential Equations (DDEs). In this paper, we leverage qualitative guarantees for the existence of an exponentially decreasing estimation on the solutions to DDEs as established in classical stability theory, and present a quantitative method for constructing such delay-dependent estimations, thereby facilitating a reduction of the verification problem over an unbounded temporal horizon to a bounded one. Our technique builds on the linearization technique of nonlinear dynamics and spectral analysis of the linearized counterparts. We show experimentally on a set of representative benchmarks from the literature that our technique indeed extends the scope of bounded verification techniques to unbounded verification tasks. Moreover, our technique is easy to implement and can be combined with any automatic tool dedicated to bounded verification of DDEs.

This work has been supported through grants by NSFC under grant No. 61625206, 61732001 and 61872341, by Deutsche Forschungsgemeinschaft through grants No. GRK 1765 and FR 2715/4, and by the CAS Pioneer Hundred Talents Program under grant No. Y8YC235015.

1 Introduction

The theory of dynamical systems featuring delayed coupling between state variables dates back to the 1920s, when Volterra [41, 42], in his research on predator-prey models and viscoelasticity, formulated some rather general differential equations incorporating the past states of the system. This formulation, now known as delay differential equations (DDEs), was developed further by, e.g., Mishkis [30] and Bellman and Cooke [2], and has witnessed numerous applications in many domains. Prominent examples include population dynamics [25], where birth rate follows changes in population size with a delay related to reproductive age; spreading of infectious diseases [5], where delay is induced by the incubation period; or networked control systems [21] with their associated transport delays when forwarding data through the communication network. These applications range further to models in optics [23], economics [38], and ecology [13], to name just a few. Albeit resulting in more accurate models, the presence of time delays in feedback dynamics often induces considerable extra complexity when one attempts to design or even verify such dynamical systems. This stems from the fact that the presence of feedback delays reduces controllability due to the impossibility of immediate reaction and enhances the likelihood of transient overshoot or even oscillation in the feedback system, thus violating safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling.

Though established automated methods addressing ordinary differential equations (ODEs) and their derived models, like hybrid automata, have been extensively studied in the verification literature, techniques pertaining to ODEs do not generalize straightforwardly to delayed dynamical systems described by DDEs. The reason is that the future evolution of a DDE is no longer governed by the current state instant only, but depends on a chunk of its historical trajectory, such that introducing even a single constant delay immediately renders a system with finite-dimensional states into an infinite-dimensional dynamical system. There are approximation methods, say the Padé approximation [39], that approximate DDEs with finite-dimensional models, which however may hide fundamental behaviors, e.g. (in-)stability, of the original delayed dynamics, as remarked in Sect. 5.2.2.8.1 of [26]. Consequently, despite well-developed numerical methods for solving DDEs as well as methods for stability analysis in the realm of control theory, hitherto in automatic verification, only a few approaches address the effects of delays due to the immediate impact of delays on the structure of the state spaces to be traversed by state-exploratory methods.

In this paper, we present a constructive approach dedicated to verifying safety properties of delayed dynamical systems encoded by DDEs, where the safety properties pertain to an infinite time domain. This problem is of particular interests when one pursues correctness guarantees concerning dynamics of safety-critical systems over a long run. Our approach builds on the linearization technique of potentially nonlinear dynamics and spectral analysis of the linearized counterparts. We leverage qualitative guarantees for the existence of an exponentially decreasing estimation on the solutions to DDEs as established in classical stability theory (see, e.g., [2, 19, 24]), and present a quantitative method to construct such estimations, thereby reducing the temporally unbounded verification problems to their bounded counterparts.

The class of systems we consider features delayed differential dynamics governed by DDEs of the form $\dot{\mathbf {x}} \left( t \right) = {\varvec{f}}\left( \mathbf {x}\left( t \right) ,\mathbf {x}\left( t-r_1 \right) ,\ldots ,\mathbf {x}\left( t-r_k \right) \right)$ with initial states specified by a continuous function ${\varvec{\phi }}\left( t\right)$ on $[-r_{\max },0]$ where $r_{\max }=\max \{r_1, \ldots , r_k\}$. It thus involves a combination of ODE and DDE with multiple constant delays $r_i > 0$, and has been successfully used to model various real-world systems in the aforementioned fields. In general, formal verification of unbounded safety or, dually, reachability properties of such systems inherits undecidability from similar properties for ODEs (cf. e.g., [14]). We therefore tackle this unbounded verification problem by leveraging a stability criterion of the system under investigation.

Contributions. In this paper, we present a quantitative method for constructing a delay-dependent, exponentially decreasing upper bound, if existent, that encloses trajectories of a DDE originating from a certain set of initial functions. This method consequently yields a temporal bound $T^*$ such that for any $T>T^*$, the system is safe over $[-r_{\max }, T]$ iff it is safe over $[-r_{\max }, \infty )$. For linear dynamics, such an equivalence of safety applies to any initial set of functions drawn from a compact subspace in $\mathbb {R}^n$; while for nonlinear dynamics, our approach produces (a subset of) the basin of attraction around a steady state, and therefore a certificate (by bounded verification in finitely many steps) that guarantees the reachable set being contained in this basin suffices to claim safety/unsafety of the system over an infinite time horizon. Our technique is easy to implement and can be combined with any automatic tool for bounded verification of DDEs. We show experimentally on a set of representative benchmarks from the literature that our technique effectively extends the scope of bounded verification techniques to unbounded verification tasks.

Related Work. As surveyed in [14], the research community has over the past three decades vividly addressed automatic verification of hybrid discrete-continuous systems in a safety-critical context. The almost universal undecidability of the unbounded reachability problem, however, confines the sound key-press routines to either semi-decision procedures or even approximation schemes, most of which address bounded verification by computing the finite-time image of a set of initial states. It should be obvious that the functional rather than state-based nature of the initial condition of DDEs prevents a straightforward generalization of this approach.

Prompted by actual engineering problems, the interest in safety verification of continuous or hybrid systems featuring delayed coupling is increasing recently. We classify these contributions into two tracks. The first track pursues propagation-based bounded verification: Huang et al. presented in [21] a technique for simulation-based time-bounded invariant verification of nonlinear networked dynamical systems with delayed interconnections, by computing bounds on the sensitivity of trajectories to changes in initial states and inputs of the system. A method adopting the paradigm of verification-by-simulation (see, e.g., [9, 16, 31]) was proposed in [4], which integrates rigorous error analysis of the numeric solving and the sensitivity-related state bloating algorithms (cf. [7]) to obtain safe enclosures of time-bounded reachable sets for systems modelled by DDEs. In [46], the authors identified a class of DDEs featuring a local homeomorphism property which facilitates construction of over- and under-approximations of reachable sets by performing reachability analysis on the boundaries of the initial sets. Goubault et al. presented in [17] a scheme to compute inner- and outer-approximating flowpipes for DDEs with uncertain initial states and parameters using Taylor models combined with space abstraction in the shape of zonotopes. The other track of the literature tackles unbounded reachability problem of DDEs by taking into account the asymptotic behavior of the dynamics under investigation, captured by, e.g., Lyapunov functions in [32, 47] and barrier certificates in [35]. These approaches however share a common limitation that a polynomial template has to be specified either for the interval Taylor models exploited in [47] (and its extension [29] to cater for properties specified as bounded metric interval temporal logic (MITL) formulae), for Lyapunov functionals in [32], or for barrier certificates in [35]. Our approach drops this limitation by resorting to the linearization technique followed by spectral analysis of the linearized counterparts, and furthermore extends over [47] by allowing immediate feedback (i.e. $\mathbf {x}(t)$) as well as multiple delays in the dynamics), to which their technique does not generalize immediately. In contrast to the absolute stability exploited in [32], namely a criterion that ensures stability for arbitrarily large delays, we give the construction of a delay-dependent stability certificate thereby substantially increasing the scope of dynamics amenable to stability criteria, for instance, the famous Wright’s equation (cf. [44]). Finally, we refer the readers to [34] and [33] for related contributions in showing the existence of abstract symbolic models for nonlinear control systems with time-varying and unknown time-delay signals via approximate bisimulations.

2 Problem Formulation

Notations. Let $\mathbb {N}$, $\mathbb {R}$ and $\mathbb {C}$ be the set of natural, real and complex numbers, respectively. Vectors will be denoted by boldface letters. For $z = a + {\mathrm {i}}b \in \mathbb {C}$ with $a,b \in \mathbb {R}$, the real and imaginary parts of z are denoted respectively by $\mathfrak {R}(z) = a$ and $\mathfrak {I}(z) = b$; $\left|z\right| = \sqrt{a^2+b^2}$ is the modulus of z. For a vector $\mathbf {x}\in \mathbb {R}^n$, $x_i$ refers to its i-th component, and its maximum norm is denoted by . We define for $\delta > 0$, as the $\delta$-closed ball around $\mathbf {x}$. The notation extends to a set $X \subseteq \mathbb {R}^n$ as , and to an $m \times n$ complex-valued matrix A as . ${}\overline{X}$ is the closure of X and $\partial X$ denotes the boundary of X. For $a \le b$, let $C^0([a,b],\mathbb {R}^n)$ denote the space of continuous functions from [a, b] to $\mathbb {R}^n$, which is associated with the maximum norm . We abbreviate $C^0([-r,0],\mathbb {R}^n)$ as $\mathcal {C}_r$ for a fixed positive constant r, and let $C^1$ consist of all continuously differentiable functions. Given $f:[0,\infty ) \mapsto \mathbb {R}$ a measurable function such that for some constants a and b, then the Laplace transform $\mathcal {L}\{f\}$ defined by $\mathcal {L}\{f\}(z) = \int _{0}^{\infty } \mathrm {e}^{- z t} f(t) {\,\mathrm{d}t}$ exists and is an analytic function of z for $\mathfrak {R}(z) > b$.

Delayed Differential Dynamics. We consider a class of dynamical systems featuring delayed differential dynamics governed by DDEs of autonomous type:

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{\mathbf {x}} \left( t \right) &{}= {\varvec{f}}\left( \mathbf {x}\left( t \right) ,\mathbf {x}\left( t-r_1 \right) ,\ldots ,\mathbf {x}\left( t-r_k \right) \right) , \quad t \in \left[ 0,\infty \right) \\ \mathbf {x}\left( t \right) &{}= {\varvec{\phi }}\left( t\right) , \quad t \in \left[ -r_k, 0 \right] \end{array}\right. \end{aligned}$$

(1)

where $\mathbf {x}$ is the time-dependent state vector in $\mathbb {R}^n$, $\dot{\mathbf {x}}$ denotes its temporal derivative $\mathrm{d}\mathbf {x}/\mathrm{d}t$, and t is a real variable modelling time. The discrete delays are assumed to be ordered as $r_k> \ldots> r_1 > 0$, and the initial states are specified by a vector-valued function ${\varvec{\phi }}\in \mathcal {C}_{r_k}$.

Suppose ${\varvec{f}}$ is a Lipschitz-continuous vector-valued function in $C^1\left( \mathbb {R}^{(k+1)n},\mathbb {R}^n\right)$, which implies that the system has a unique maximal solution (or trajectory) from a given initial condition ${\varvec{\phi }}\in \mathcal {C}_{r_k}$, denoted as ${\varvec{\xi }}_{{\varvec{\phi }}}:[-r_k, \infty ) \mapsto \mathbb {R}^n$. We denote in the sequel by the Jacobian matrix (i.e., matrix consisting of all first-order partial derivatives) of ${\varvec{f}}$ w.r.t. the component $\mathbf {x}\left( t\right)$. Similar notations apply to components $\mathbf {x}\left( t-r_i \right)$, for $i = 1, \ldots , k$.

Example 1

(Gene regulation [12, 36]). The control of gene expression in cells is often modelled with time delays in equations of the form

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{x_1}(t) &{}= g\left( x_n(t-r_n)\right) - \beta _1 x_1(t) \\ \dot{x_j}(t) &{}= x_{j-1}(t-r_{j-1}) - \beta _j x_j(t), \quad 1 < j \le n \end{array}\right. \end{aligned}$$

(2)

where the gene is transcribed producing mRNA ($x_1$), which is translated into enzyme $x_2$ that in turn produces another enzyme $x_3$ and so on. The end product $x_n$ acts to repress the transcription of the gene by $\dot{g} < 0$. Time delays are introduced to account for time involved in transcription, translation, and transport. The positive $\beta _j$’s represent decay rates of the species. The dynamic described in Eq. (2) falls exactly into the scope of systems considered in this paper, and in fact, it instantiates a more general family of systems known as monotone cyclic feedback systems (MCFS) [28], which includes neural networks, testosterone control, and many other effects in systems biology.

Lyapunov Stability. Given a system of DDEs in Eq. (1), suppose ${\varvec{f}}$ has a steady state (a.k.a., equilibrium) at $\mathbf {x}_e$ such that ${\varvec{f}}(\mathbf {x}_e,\ldots ,\mathbf {x}_e) = \mathbf {0}$ then

• $\mathbf {x}_e$ is said to be Lyapunov stable, if for every $\epsilon > 0$, there exists $\delta > 0$ such that, if , then for every $t \ge 0$ we have .

• $\mathbf {x}_e$ is said to be asymptotically stable, if it is Lyapunov stable and there exists $\delta > 0$ such that, if , then .

• $\mathbf {x}_e$ is said to be exponentially stable, if it is asymptotically stable and there exist $\alpha ,\beta ,\delta > 0$ such that, if , then , for all $t \ge 0$. The constant $\beta$ is called the rate of convergence.

Here $\mathbf {x}_e$ can be generalized to a constant function in $\mathcal {C}_{r_k}$ when employing the supremum norm over functions. This norm further yields the locality of the above definitions, i.e., they describe the behavior of a system near an equilibrium, rather than of all initial conditions ${\varvec{\phi }}\in \mathcal {C}_{r_k}$, in which case it is termed the global stability. W.l.o.g., we assume ${\varvec{f}}(\mathbf {0},\ldots ,\mathbf {0}) = \mathbf {0}$ in the sequel and investigate the stability of the zero equilibrium thereof. Any nonzero equilibrium can be straightforwardly shifted to a zero one by coordinate transformation while preserving the stability properties, see e.g., [19].

Safety Verification Problem. Given $\mathcal {X}\subseteq \mathbb {R}^n$ a compact set of initial states and $\mathcal {U}\subseteq \mathbb {R}^n$ a set of unsafe or otherwise bad states, a delayed dynamical system of the form (1) is said to be $T$-safe iff all trajectories originating from any ${\varvec{\phi }}(t)$ satisfying ${\varvec{\phi }}(t) \in \mathcal {X}, \forall t \in [-r_k,0]$ do not intersect with $\mathcal {U}$ at any $t \in [-r_k, T]$, and $T$-unsafe otherwise. In particular, we distinguish unbounded verification with $T= \infty$ from bounded verification with $T< \infty$.

In subsequent sections, we first present our approach to tackling the safety verification problem of delayed differential dynamics coupled with one single constant delay (i.e., $k=1$ in Eq. (1)) in an unbounded time domain, by leveraging a quantitative stability criterion, if existent, for the linearized counterpart of the potentially nonlinear dynamics in question. A natural extension of this approach to cater for dynamics with multiple delay terms will be remarked thereafter. In what follows, we start the elaboration of the method from DDEs of linear dynamics that admit spectral analysis, and move to nonlinear cases afterwards and show how the linearization technique can be exploited therein.

3 Linear Dynamics

Consider the linear sub-class of dynamics given in Eq. (1):

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{\mathbf {x}} \left( t \right) &{}= A \mathbf {x}\left( t \right) + B \mathbf {x}\left( t-r \right) , \quad t \in \left[ 0,\infty \right) \\ \mathbf {x}\left( t \right) &{}= {\varvec{\phi }}\left( t\right) , \quad t \in \left[ -r,0 \right] \end{array}\right. \end{aligned}$$

(3)

where $A,B \in \mathbb {R}^{n \times n}$, ${\varvec{\phi }}\in \mathcal {C}_r$, and the system is associated with the characteristic equation

$$\begin{aligned} \det \left( z I - A - B \mathrm {e}^{-r z}\right) = 0, \end{aligned}$$

(4)

where I is the $n \times n$ identity matrix. Denote by the characteristic matrix in the sequel. Notice that the characteristic equation can be obtained by seeking nontrivial solutions to Eq. (3) of the form ${\varvec{\xi }}_{{\varvec{\phi }}}(t) = \mathbf {c} \mathrm {e}^{z t}$, where $\mathbf {c}$ is an n-dimensional nonzero constant vector.

The roots $\lambda \in \mathbb {C}$ of Eq. (4) are called characteristic roots or eigenvalues and the set of all eigenvalues is referred to as the spectrum, denoted by $\sigma = \{\lambda \mid \det \left( h(\lambda )\right) = 0\}$. Due to the exponentiation in the characteristic equation, the DDE has, in line with its infinite-dimensional nature, infinitely many eigenvalues possibly, making a spectral analysis more involved. The spectrum does however enjoy some elementary properties that can be exploited in the analysis. For instance, the spectrum has no finite accumulation point in $\mathbb {C}$ and therefore for each positive $\gamma \in \mathbb {R}$, the number of roots satisfying $\left|\lambda \right| \le \gamma$ is finite. It follows that the spectrum is a countable (albeit possibly infinite) set:

Lemma 1

(Accumulation freedom [6, 19]). Given $\gamma \in \mathbb {R}$, there are at most finitely many characteristic roots satisfying $\mathfrak {R}(\lambda ) > \gamma$. If there is a sequence $\{\lambda _n\}$ of roots of Eq. (4) such that $\left|\lambda _n\right| \rightarrow \infty$ as $n \rightarrow \infty$, then $\mathfrak {R}(\lambda _n) \rightarrow -\infty$ as $n \rightarrow \infty$.

Lemma 1 suggests that there are only a finite number of solutions in any vertical strip in the complex plane, and there thus exists an upper bound $\alpha \in \mathbb {R}$ such that every characteristic root $\lambda$ in the spectrum satisfies $\mathfrak {R}(\lambda ) < \alpha$. This upper bound captures essentially the asymptotic behavior of the linear dynamics:

Theorem 1

(Globally exponential stability [6, 36]). Suppose $\mathfrak {R}(\lambda ) < \alpha$ for every characteristic root $\lambda$. Then there exists $K > 0$ such that

(5)

where ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ is the solution to Eq. (3). In particular, $\mathbf {x}= \mathbf {0}$ is a globally exponentially stable equilibrium of Eq. (3) if $\mathfrak {R}(\lambda ) < 0$ for every characteristic root; it is unstable if there is a root satisfying $\mathfrak {R}(\lambda ) > 0$.

Theorem 1 establishes an existential guarantee that the solution to the linear delayed dynamics approaches the zero equilibrium exponentially for any initial conditions in $\mathcal {C}_r$. To achieve automatic safety verification, however, we ought to find a constructive means of estimating the (signed) rate of convergence $\alpha$ and the coefficient K in Eq. (5). This motivates the introduction of the so-called fundamental solution ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ to Eq. (3), whose Laplace transform will later be shown to be $h^{-1}(z)$, the inverse characteristic matrix, which always exists for z satisfying $\mathfrak {R}(z) > \max _{\lambda \in \sigma } \mathfrak {R}(\lambda )$.

Lemma 2

(Variation-of-constants [19, 36]). Let ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ be the solution to Eq. (3). Denote by ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ the solution that satisfies Eq. (3) for $t \ge 0$ and satisfies a variation of the initial condition as ${\varvec{\phi }}'(0) = I$ and ${\varvec{\phi }}'(t) = O$ for all $t \in [-r,0)$, where $O$ is the $n \times n$ zero matrix, then for $t \ge 0$,

$$\begin{aligned} {\varvec{\xi }}_{{\varvec{\phi }}}(t) = {\varvec{\xi }}_{{\varvec{\phi }}'}(t) {\varvec{\phi }}(0) + \int _0^t {\varvec{\xi }}_{{\varvec{\phi }}'} (t - \tau ) B{\varvec{\phi }}(\tau - r) {\,\mathrm{d}\tau }. \end{aligned}$$

(6)

Note that in Eq. (6), ${\varvec{\phi }}(t)$ is extended to $[-r, \infty )$ by making it zero for $t > 0$. In spite of the discontinuity of ${\varvec{\phi }}'$ at zero, the existence of the solution ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ can be proven by the well-known method of steps [8].

Lemma 3

(Fundamental solution [19]). The solution ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ to Eq. (3) with initial data ${\varvec{\phi }}'$ is the fundamental solution; that is for z s.t. $\mathfrak {R}(z) > \max _{\lambda \in \sigma } \mathfrak {R}(\lambda )$,

$$\begin{aligned} \mathcal {L}\{{\varvec{\xi }}_{{\varvec{\phi }}'}\}(z) = h^{-1}(z). \end{aligned}$$

The fundamental solution ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ can be proven to share the same exponential bound as that in Theorem 1, while the following theorem, as a consequence of Lemma 2, gives an exponential estimation of ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ in connection with ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$:

Theorem 2

(Exponential estimation [36]). Denote by the maximum real part of eigenvalues in the spectrum. Then for any $\alpha > \mu$, there exists $K > 0$ such that

(7)

and hence by Eq. (6), for any $t \ge 0$ and ${\varvec{\phi }}\in \mathcal {C}_r$. In particular, $\mathbf {x}= \mathbf {0}$ is globally exponentially stable for Eq. (3) if $\mu < 0$.

Following Theorem 2, an exponentially decreasing bound on the solution ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ to linear DDEs of the form (3) can be assembled by computing $\alpha$ satisfying $\mu< \alpha < 0$ and the coefficient $K > 0$.

3.1 Identifying the Rightmost Roots

Due to the significance of characteristic roots in the context of stability and bifurcation analysis, numerical methods on identifying—particularly the rightmost—roots of linear (or linearized) DDEs have been extensively studied in the past few decades, see e.g., [3, 11, 43, 45]. There are indeed complete methods on isolating real roots of polynomial exponential functions, for instances [37] and [15] based on cylindrical algebraic decomposition (CAD). Nevertheless, as soon as non-trivial exponential functions arise in the characteristic equation, there appear to be few, if any, symbolic approaches to detecting complex roots of the equation.

In this paper, we find $\alpha$ that bounds the spectrum from the right of the complex plane, by resorting to the numerical approach developed in [11]. The computation therein employs discretization of the solution operator using linear multistep (LMS) methods to approximate eigenvalues of linear DDEs with multiple constant delays, under an absolute error of $\mathcal {O}\left( \tau ^p\right)$ for sufficiently small stepsize $\tau$, where $\mathcal {O}\left( \cdot \right)$ is the big Omicron notation and p depends on the order of the LMS-methods. A well-developed Matlab package called DDE-BIFTOOL [10] is furthermore available to mechanize the computation, which will be demonstrated in our forthcoming examples.

3.2 Constructing K

By the inverse Laplace transform (cf. Theorem 5.2 in [19] for a detailed proof), we have ${\varvec{\xi }}_{{\varvec{\phi }}'}(t) = \lim _{V \rightarrow \infty } \frac{1}{2 \pi {\mathrm {i}}} \int _{\alpha - {\mathrm {i}}V}^{\alpha + {\mathrm {i}}V} \mathrm {e}^{z t} h^{-1}(z) {\,\mathrm{d}z}$ for z satisfying $\mathfrak {R}(z) > \mu$, where $\alpha$ is the exponent associated with the bound on ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ in Eq. (7), and hence by substituting $z = \alpha + {\mathrm {i}}\nu$, we have

$$\begin{aligned} \mathrm {e}^{-\alpha t} {\varvec{\xi }}_{{\varvec{\phi }}'}(t) = \lim _{V \rightarrow \infty } \frac{1}{2 \pi } \int _{-V}^{V} \mathrm {e}^{{\mathrm {i}}\nu t} h^{-1}(\alpha + {\mathrm {i}}\nu ) {\,\mathrm{d}\nu }. \end{aligned}$$

Since $h^{-1}(z) = \frac{I}{z} + \left( h^{-1}(z) -\frac{I}{z}\right) = \frac{I}{z} + \mathcal {O}\left( 1/z^2\right)$, together with the fact that an integral over a quadratic integrand is convergent, it follows that

$$\begin{aligned} \mathrm {e}^{-\alpha t} {\varvec{\xi }}_{{\varvec{\phi }}'}(t) = \lim _{V \rightarrow \infty } \frac{1}{2 \pi } \int _{-V}^{V} \mathrm {e}^{{\mathrm {i}}\nu t} \frac{I}{\alpha + {\mathrm {i}}\nu } {\,\mathrm{d}\nu } + \frac{1}{2 \pi } \int _{-\infty }^{\infty } \mathrm {e}^{{\mathrm {i}}\nu t} \mathcal {O}\left( \frac{1}{(\alpha + {\mathrm {i}}\nu )^2}\right) {\,\mathrm{d}\nu }. \end{aligned}$$

By taking the norm while observing that $\left|\mathrm {e}^{{\mathrm {i}}\nu t}\right| = 1$, we get

(8)

For the integral (8-a), the fact¹ that

$$\begin{aligned} \int _{-\infty }^{\infty }\frac{\mathrm {e}^{{\mathrm {i}}a x}}{b + {\mathrm {i}}x}{\,\mathrm{d}x} =\int _{-\infty }^{\infty }\frac{\mathrm {e}^{{\mathrm {i}}x}}{a b + {\mathrm {i}}x}{\,\mathrm{d}x} ={\left\{ \begin{array}{ll} 2\pi \mathrm {e}^{-a b} &{} \text {if}\ a, b> 0\\ 0 &{} \text {if}\ a > 0, b < 0, \end{array}\right. } \end{aligned}$$

(9)

implies

(10)

Notice that the second integral (8-b) is computable, since it is convergent and independent of t. The underlying computation of the improper integral, however, can be rather time-consuming. We therefore detour by computing an upper bound of (8-b) in the form of a definite integral, due to Lemma 4, which suffices to constitute an exponential estimation of ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ while reducing computational efforts pertinent to the integration.

Lemma 4

There exists $M > 0$ such that inequation (11) below holds for any $\alpha > \mu$.

(11)

where , $z=\alpha + {\mathrm {i}}\nu$, and n is the order of A and B.

Proof

The proof depends essentially on constructing a threshold $M > 0$ such that the integral over $\left|\nu \right| > M$ can be bounded, thus transforming the improper integral in question to a definite one. To find such an M, observe that

Without loss of generality, suppose the entry of $h^{-1}(z)$ at (i, j) takes the form

$$\begin{aligned}&\left( h^{-1}\right) _{i j} =(\sum _{k=0}^{n-1}p^{i j}_k(\mathrm {e}^{-r z})z^k)/ \det (h(z)) =(\sum _{k=0}^{n-1}p^{i j}_k(\mathrm {e}^{-r z})z^k)/ (z^n+\sum _{k=0}^{n-1}q_k(\mathrm {e}^{-r z})z^k) \\&\qquad \qquad \qquad \qquad \qquad \qquad =\frac{1}{z}\, (\sum \limits _{k=0}^{n-1}p^{i j}_k(\mathrm {e}^{-r z}) z^{k-n+1})/(1+\sum \limits _{k=0}^{n-1}q_k(\mathrm {e}^{-r z})z^{k-n}), \end{aligned}$$

where $p^{i j}_k(\cdot )$ and $q_k(\cdot )$ are polynomials in $\mathrm {e}^{-r z}$ as coefficients of $z^k$. Since $\mathrm {e}^{-r z}$ is bounded by $\mathrm {e}^{-r \alpha }$ along the vertical line $z = \alpha + {\mathrm {i}}\nu$, we can conclude that there exist $P^{i j}_k$ and $Q_k$ such that $\left|p^{i j}_k (\mathrm {e}^{-r z})\right| \le P^{i j}_k$ and $\left|q_k (\mathrm {e}^{-r z})\right| \le Q_k$, with $P^{i j}_{n-1} = 1$ if $i = j$, and 0 otherwise. Furthermore, in the vertical line $z = \alpha + {\mathrm {i}}\nu$, if $\left|\nu \right| \ge 1$, then

$$\begin{aligned}&\left|\sum _{k=0}^{n-1} p^{i j}_k (\mathrm {e}^{-r z}) z^{k-n+1}\right| \le \left|p^{i j}_{n-1} (\mathrm {e}^{-r z})\right| + \sum _{k=0}^{n-2} \left|p^{i j}_k(\mathrm {e}^{-r z}) z^{-1}\right| \le P^{i j}_{n-1} + \sum _{k=0}^{n-2} P^{i j}_k \left|z^{-1}\right|,\\&\,\,\,\qquad \left|1 + \sum _{k=0}^{n-1}q_k (\mathrm {e}^{-r z}) z^{k-n}\right| \ge 1 - \sum _{k=0}^{n-1} \left|q_k (\mathrm {e}^{-r z})\right| \left|z^{k-n}\right| \ge 1 - \sum _{k=0}^{n-1} Q_k \left|z^{-1}\right|. \end{aligned}$$

We can thus choose , which implies

$$\begin{aligned}&\left|(\sum _{k=0}^{n-1} p^{i j}_k (\mathrm {e}^{-r z}) z^k)/\det (h(z))\right| \le \left|\frac{1}{z} (\sum _{k=0}^{n-1} p^{i j}_k (\mathrm {e}^{-r z})z^{k-n+1})/(1 + \sum _{k=0}^{n-1} q_k (\mathrm {e}^{-r z}) z^{k-n})\right|\\&\qquad \qquad \le \left|\frac{1}{z}\right|(P^{i j}_{n-1}+\sum _{k=0}^{n-2} P^{i j}_k \left|z^{-1}\right|)/(1 - \sum _{k=0}^{n-1} Q_k \left|z^{-1}\right|) \le \frac{2}{\left|z\right|}(1 + P^{i j}_{n-1}) \le \frac{4}{\left|z\right|}, \end{aligned}$$

where the third inequality holds since $\left|\nu \right|>M$. It then follows, if $\left|\nu \right| > M$, that

and thereby

This completes the proof. $\square$

Equations (8), (10) and (11) yield that is upper-bounded by

(12)

for all $t > 0$. Here M is the constant given in Lemma 4, while $1_0:(\mu , \infty )\setminus \{0\} \mapsto \{0, 1\}$ is an indicator function² of $\{\alpha \mid \alpha > 0\}$, i.e., $1_0(\alpha ) = 1$ for $\alpha > 0$ and $1_0(\alpha ) = 0$ for $\mu< \alpha < 0$.

In contrast to the existential estimation guarantee established in Theorem 2, exploiting the construction of $\alpha$ and K gives a constructive quantitative criterion permitting to reduce an unbounded safety verification problem to its bounded counterpart:

Theorem 3

(Equivalence of bounded and unbounded safety). Given $\mathcal {X}\subseteq \mathbb {R}^n$ a set of initial states and $\mathcal {U}\subseteq \mathbb {R}^n$ a set of bad states satisfying $\mathbf {0}\notin {}\overline{\mathcal {U}}$, suppose we have $\alpha$ satisfying $\mu< \alpha < 0$ and K from Eq. (12). Let , then there exists $T^* < \infty$, defined as

(13)

such that for any $T > T^*$, the system (3) is $\infty$-safe iff it is T-safe.

Proof

The “only if” part is for free, as $\infty$-safety subsumes by definition T-safety. For the “if” direction, the constructed K in Eq. (12) suffices as an upper bound of , and hence by Theorem 2, for any $t \ge 0$ and ${\varvec{\phi }}$ constrained by $\mathcal {X}$. As a consequence, it suffices to show that $T^*$ given by Eq. (13) is finite, which then by definition implies that system (3) is safe over $t > T^*$. Note that the assumption $\mathbf {0}\notin {}\overline{\mathcal {U}}$ implies that there exists a ball $\mathcal {B}(\mathbf {0},\delta )$ such that $\mathcal {B}(\mathbf {0},\delta ) \cap \mathcal {U}= \emptyset$. Moreover, $\hat{K} \mathrm {e}^{\alpha t}$ is strictly monotonically decreasing w.r.t. t, and thus $T = \max \{0, \ln (\delta /\hat{K})/\alpha \}$ is an upper bound³ of $T^*$, which further implies $T^* < \infty$. $\square$

Example 2

(PD-controller [17]). Consider a PD-controller with linear dynamics defined, for $t \ge 0$, as

$$\begin{aligned} \dot{y}(t) = v(t); \quad \dot{v}(t) = - \kappa _p \left( y(t - r) - y^* \right) - \kappa _d v(t - r), \end{aligned}$$

(14)

which controls the position y and velocity v of an autonomous vehicle by adjusting its acceleration according to the current distance to a reference position $y^*$. A constant time delay r is introduced to model the time lag due to sensing, computation, transmission, and/or actuation. We instantiate the parameters following [17] as $\kappa _p = 2$, $\kappa _d = 3$, $y^* = 1$, and $r = 0.35$. The system described by Eq. (14) then has one equilibrium at (1; 0), which shares equivalent stability with the zero equilibrium of the following system, with $\hat{y} = y - 1$ and $\hat{v} = v$:

$$\begin{aligned} \dot{\hat{y}}(t) = \hat{v}(t); \quad \dot{\hat{v}}(t) = - 2 \hat{y}(t - r) - 3 \hat{v}(t - r). \end{aligned}$$

(15)

Suppose we are interested in exploiting the safety property of the system (15) in an unbounded time domain, relative to the set of initial states $\mathcal {X}= [- 0.1, 0.1] \times [0, 0.1]$ and the set of unsafe states $\mathcal {U}=\{(\hat{y};\hat{v}) \mid \left|\hat{y}\right| > 0.2\}$. Following our construction process, we obtain automatically some key arguments (depicted in Fig. 1) as $\alpha = - 0.5$, $M = 11.9125$, $K = 7.59162$ and $\hat{K} = 2.21103$, which consequently yield $T^* = 4.80579\,\hbox {s}$. By Theorem 3, the unbounded safety verification problem thus is reduced to a T-bounded one for any $T > T^*$, inasmuch as $\infty$-safety is equivalent to T-safety for the underlying dynamics.

$[-\hat{K} \mathrm {e}^{\alpha t}, \hat{K} \mathrm {e}^{\alpha t}]^n$ in Eq. (13) can be viewed as an overapproximation of all trajectories originating from $\mathcal {X}$. As shown in the right part of Fig. 1, this overapproximation, however, is obviously too conservative to be utilized in proving or disproving almost any safety specifications of practical interest. The contribution of our approach lies in the reduction of unbounded verification problems to their bounded counterparts, thereby yielding a quantitative time bound $T^*$ that substantially “trims off” the verification efforts pertaining to $t > T^*$. The derived T-safety verification task can be tackled effectively by methods dedicated to bounded verification of DDEs of the form (3), or more generally, (1), e.g., approaches in [17] and [4].

Fig. 1.

Left: the identified rightmost roots of h(z) in DDE-BIFTOOL and an upper bound $\alpha = -0.5$ such that $\max _{\lambda \in \sigma } \mathfrak {R}(\lambda )< \alpha < 0$; Center: $M = 11.9125$ that suffices to split and hence upper-bound the improper integral in Eq. (11); Right: the obtained time instant $T^* = 4.80579$ s guaranteeing the equivalence of $\infty$-safety and T-safety of the PD-controller, for any $T > T^*$.

4 Nonlinear Dynamics

In this section, we address a more general form of dynamics featuring substantial nonlinearity, by resorting to linearization techniques and thereby establishing a quantitative stability criterion, analogous to the linear case, for nonlinear delayed dynamics.

Consider a singly delayed version of Eq. (1):

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{\mathbf {x}} \left( t \right) &{}= {\varvec{f}}\left( \mathbf {x}\left( t \right) ,\mathbf {x}\left( t-r \right) \right) , \quad t \in \left[ 0,\infty \right) \\ \mathbf {x}\left( t \right) &{}= {\varvec{\phi }}\left( t\right) , \quad t \in \left[ -r, 0 \right] \end{array}\right. \end{aligned}$$

(16)

with ${\varvec{f}}$ being a nonlinear vector field involving possibly non-polynomial functions. Let

$$\begin{aligned} {\varvec{f}}\left( \mathbf {x}, \mathbf {y}\right) = A \mathbf {x}+ B \mathbf {y}+ {\varvec{g}}(\mathbf {x}, \mathbf {y}), \text { with } A = {\varvec{f}}_\mathbf {x}\left( \mathbf {0}, \mathbf {0}\right) , B = {\varvec{f}}_\mathbf {y}\left( \mathbf {0}, \mathbf {0}\right) , \end{aligned}$$

where ${\varvec{f}}_\mathbf {x}$ and ${\varvec{f}}_\mathbf {y}$ are the Jacobian matrices of ${\varvec{f}}$ in terms of $\mathbf {x}$ and $\mathbf {y}$, respectively; ${\varvec{g}}$ is a vector-valued, high-order term whose Jacobian matrix at $\left( \mathbf {0}, \mathbf {0}\right)$ is $O$.

By dropping the high-order term ${\varvec{g}}$ in ${\varvec{f}}$, we get the linearized counterpart of Eq. (16):

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{\mathbf {x}} \left( t \right) &{}= A \mathbf {x}\left( t \right) + B \mathbf {x}\left( t-r \right) , \quad t \in \left[ 0,\infty \right) \\ \mathbf {x}\left( t \right) &{}= {\varvec{\phi }}\left( t\right) , \quad t \in \left[ -r, 0 \right] \end{array}\right. \end{aligned}$$

(17)

which falls in the scope of linear dynamics specified in Eq. (3), and therefore is associated with a characteristic equation of the same form as that in Eq. (4). Equation (17) will be in the sequel referred to as the linearization of Eq. (16) at the steady state $\mathbf {0}$, and $\sigma$ is used to denote the spectrum of the characteristic equation corresponding to Eq. (17).

In light of the well-known Hartman-Grobman theorem [18, 20] in the realm of dynamical systems, the local behavior of a nonlinear dynamical system near a (hyperbolic) equilibrium is qualitatively the same as that of its linearization near this equilibrium. The following statement uncovers the connection between the locally asymptotic behavior of a nonlinear system and the spectrum of its linearization:

Theorem 4

(Locally exponential stability [6, 36]). Suppose $\max _{\lambda \in \sigma } \mathfrak {R}(\lambda )< \alpha < 0$. Then $\mathbf {x}= \mathbf {0}$ is a locally exponentially stable equilibrium of the nonlinear systems (16). In fact, there exists $\delta > 0$ and $K > 0$ such that

where ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ is the solution to Eq. (16). If $\mathfrak {R}(\lambda ) > 0$ for some $\lambda$ in $\sigma$, then $\mathbf {x}= \mathbf {0}$ is unstable.

Akin to the linear case, Theorem 4 establishes an existential guarantee that the solution to the nonlinear delayed dynamics approaches the zero equilibrium exponentially for initial conditions within a $\delta$-neighborhood of this equilibrium. The need of constructing $\alpha$, K and $\delta$ quantitatively in Theorem 4, as essential to our automatic verification approach, invokes again the fundamental solution ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ to the linearized dynamics in Eq. (17):

Lemma 5

(Variation-of-constants [19, 36]). Consider nonhomogeneous systems of the form

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{\mathbf {x}} \left( t \right) &{}= A \mathbf {x}\left( t \right) + B \mathbf {x}\left( t-r \right) + \varvec{\eta } \left( t \right) , \quad t \in \left[ 0,\infty \right) \\ \mathbf {x}\left( t \right) &{}= {\varvec{\phi }}\left( t\right) , \quad t \in \left[ -r, 0 \right] \end{array}\right. \end{aligned}$$

(18)

Let ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ be the solution to Eq. (18). Denote by ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ the solution that satisfies Eq. (17) for $t \ge 0$ and satisfies a variation of the initial condition as ${\varvec{\phi }}'(0) = I$ and ${\varvec{\phi }}'(t) = O$ for all $t \in [-r,0)$. Then for $t \ge 0$,

$$\begin{aligned} {\varvec{\xi }}_{{\varvec{\phi }}}(t) = {\varvec{\xi }}_{{\varvec{\phi }}'}(t) {\varvec{\phi }}(0) + \int _0^t {\varvec{\xi }}_{{\varvec{\phi }}'} (t - \tau ) B {\varvec{\phi }}(\tau - r) {\,\mathrm{d}\tau } + \int _0^t {\varvec{\xi }}_{{\varvec{\phi }}'} (t - \tau ) \varvec{\eta } (\tau ) {\,\mathrm{d}\tau }, \end{aligned}$$

(19)

where ${\varvec{\phi }}$ is extended to $[-r, \infty )$ with ${\varvec{\phi }}(t) = 0$ for $t > 0$.

In what follows, we give a constructive quantitative estimation of the solutions to nonlinear dynamics, which admits a reduction of the problem of constructing an exponential upper bound of a nonlinear system to that of its linearization, as being immediately evident from the constructive proof.

Theorem 5

(Exponential estimation). Suppose that $\max _{\lambda \in \sigma } \mathfrak {R}(\lambda )< \alpha < 0$. Then there exist $K>0$ and $\delta > 0$ such that for any $t \ge 0$, and

where ${\varvec{\xi }}_{{\varvec{\phi }}}(t)$ is the solution to nonlinear systems (16) and ${\varvec{\xi }}_{{\varvec{\phi }}'}(t)$ is the fundamental solution to the linearized counterpart (17).

Proof

The existence of K follows directly from Eq. (7) in Theorem 2. By the variation-of-constants formula (19), we have, for $t \ge 0$,

$$\begin{aligned} {\varvec{\xi }}_{{\varvec{\phi }}}(t) = {\varvec{\xi }}_{{\varvec{\phi }}'}(t) {\varvec{\phi }}(0) + \int _0^t {\varvec{\xi }}_{{\varvec{\phi }}'} (t - \tau ) B {\varvec{\phi }}(\tau - r) {\,\mathrm{d}\tau } + \int _0^t {\varvec{\xi }}_{{\varvec{\phi }}'} (t - \tau ) {\varvec{g}}(\mathbf {x}(\tau ), \mathbf {x}(\tau -r)) {\,\mathrm{d}\tau }, \end{aligned}$$

(20)

where ${\varvec{\phi }}$ is extended to $[-r, \infty )$ with ${\varvec{\phi }}(t) = 0$ for $t > 0$. Define $\mathbf {x}_t^{\varvec{\phi }}(\cdot ) \in \mathcal {C}_r$ as $\mathbf {x}_t^{\varvec{\phi }}(\theta ) = {\varvec{\xi }}_{{\varvec{\phi }}}(t+\theta )$ for $\theta \in [-r, 0]$. Then ${\varvec{g}}(\cdot ,\cdot )$ being a higher-order term yields that for any $\epsilon > 0$, there exists $\delta _\epsilon > 0$ such that implies . Due to the fact that and the monotonicity of with $\alpha < 0$, we have . This, together with Eq. (20), leads to

Hence,

By the Grönwall-Bellman inequality [1] we obtain

and thus

Set $\epsilon \le -\alpha / (2 K \mathrm {e}^{-r \alpha })$ and . This yields, for any $t \ge 0$,

completing the proof. $\square$

The above constructive quantitative estimation of the solutions to nonlinear dynamics gives rise to the reduction, analogous to the linear case, of unbounded verification problems to bounded ones, in the presence of a local stability criterion.

Theorem 6

(Equivalence of safety properties). Given initial state set $\mathcal {X}\subseteq \mathbb {R}^n$ and bad states $\mathcal {U}\subseteq \mathbb {R}^n$ satisfying $\mathbf {0}\notin {}\overline{\mathcal {U}}$. Let $\sigma$ denote the spectrum of the characteristic equation corresponding to Eq. (17). Suppose that $\max _{\lambda \in \sigma } \mathfrak {R}(\lambda )< \alpha < 0$, and the fundamental solution to Eq. (17) satisfies for any $t\ge 0$. Let . Then there exists $\delta > 0$ and $T^* < \infty$, defined as

such that if , then for any $T > T^*$, the system (16) is $\infty$-safe iff it is T-safe.

Proof

The proof is analogous to that of Theorem 3, particularly following from the local stability property stated in Theorem 5. $\square$

Note that for nonlinear dynamics, the equivalence of safety claimed by Theorem 6 holds on the condition that , due to the locality stemming from linearization. In fact, such a set $\mathfrak {B}\subseteq \mathbb {R}^n$ satisfying describes (a subset of) the basin of attraction around the local attractor $\mathbf {0}$, in a sense that any initial condition in $\mathfrak {B}$ will lead the trajectory eventually into the attractor. Consequently, for verification problems where $\mathcal {X}\supseteq \mathfrak {B}$, if the reachable set originating from $\mathcal {X}$ is guaranteed to be subsumed within $\mathfrak {B}$ in the time interval $[T'-r, T']$, then $T'+T^*$ suffices as a bound to avoid unbounded verification, namely for any $T > T'+T^*$, the system is $\infty$-safe iff it is T-safe. This is furthermore demonstrated by the following example.

Example 3

(Population dynamics [4, 25]). Consider a slightly modified version of the delayed logistic equation introduced by G. Hutchinson in 1948 (cf. [22])

$$\begin{aligned} \dot{N}(t) = N(t) [1-N(t-r)], \quad t \ge 0, \end{aligned}$$

(21)

which is used to model a single population whose percapita rate of growth $\dot{N}(t) / N(t)$ depends on the population size r time units in the past. This would be a reasonable model for a population that features a significant minimum reproductive age or depends on a resource, like food, needing time to grow and thus to recover its availability.

If we change variables, putting $u = N-1$, then Eq. (21) becomes the famous Wright’s equation (see [44]):

$$\begin{aligned} \dot{u}(t) = -u(t-r) [ 1 + u(t)], \quad t \ge 0. \end{aligned}$$

(22)

The steady state $N = 1$ is now $u = 0$. We instantiate the verification problem of Eq. (22) over $[-r, \infty )$ as $\mathcal {X}= [-0.2, 0.2]$, $\mathcal {U}= \{ u \mid \left|u\right| > 0.6 \}$, under a constant delay $r = 1$. Note that delay-independent Lyapunov techniques, e.g. [32], cannot solve this problem, since Wright’s conjecture [44], which has been recently proven in [40], together with corollaries thereof implies that there does not exist a Lyapunov functional guaranteeing absolute stability of Eq. (22) with arbitrary constant delays. To achieve an exponential estimation, we first linearize the dynamics by dropping the nonlinearity $u(t) u(t-r)$ thereof:

$$\begin{aligned} \dot{v}(t) = -v(t-1), \quad t \ge 0. \end{aligned}$$

(23)

Following our constructive approach, we obtain automatically for Eq. (23) $\alpha = -0.3$ (see the left of Fig. 2), $M = 2.69972$, $K = 3.28727$, and thereby for Eq. (22) $\delta = 0.00351678$, $\tilde{K} = 0.0338039$ and $T^* = 0\,\hbox {s}$. It is worth highlighting that by the bounded verification method in [17], with Taylor models of the order 5, an overapproximation $\varOmega$ of the reachable set w.r.t. system (22) over the time interval [14.5, 15.5] was verified to be enclosed in the $\delta$-neighborhood of $\mathbf {0}$, i.e., , yet escaped from this region around $t = 55.3$ s, and tended to diverge soon, as depicted in the right part of Fig. 2, and thus cannot prove unbounded safety properties. However, with our result of $T^* = 0\hbox {s}$ and the fact that $\varOmega$ over $[-1,15.5]$ is disjoint with $\mathcal {U}$, we are able to claim safety of the underlying system over an infinite time domain.

Fig. 2.

Left: the identified rightmost eigenvalues of h(z) and an upper bound $\alpha = -0.5$ such that $\max _{\lambda \in \sigma } \mathfrak {R}(\lambda )< \alpha < 0$; Right: overapproximation of the reachable set of the system (22) produced by the method in [17] using Taylor models for bounded verification. Together with this overapproximation we prove the equivalence of $\infty$-safety and T-safety of the system, for any $T > (T'+T^*) = 15.5\,\hbox {s}$.

DDEs with Multiple Different Delays. Delay differential equations with multiple fixed discrete delays are extensively used in the literature to model practical systems where components coupled with different time lags coexist and interact with each other. We remark that previous theorems on exponential estimation and equivalence of safety w.r.t. cases of single delay extend immediately to systems of the form (1) with almost no change, except for replacing with and with , where $A_i$ denotes the matrix attached to $\mathbf {x}(t - r_i)$ in the linearization. For a slightly modified form of the variation-of-constants formula under multiple delays, we refer the readers to Theorem 1.2 in [19].

5 Implementation and Experimental Results

To further investigate the scalability and efficiency of our constructive approach, we have carried out a prototypical implementation⁴ in Wolfram Mathematica, which was selected due to its built-in primitives for integration and matrix operations. By interfacing with DDE-BIFTOOL⁵ (in Matlab or GNU Octave) for identifying the rightmost characteristic roots of linear (or linearized) DDEs, our implementation computes an appropriate $T^*$ that admits a reduction of unbounded verification problems to bounded ones. A set of benchmark examples from the literature has been evaluated on a 3.6 GHz Intel Core-i7 processor with 8 GB RAM running 64-bit Ubuntu 16.04. All computations of $T^*$ were safely rounded and finished within 6 s for any of the examples, including Examples 2 and 3. In what follows, we demonstrate in particular the applicability of our technique to DDEs featuring non-polynomial dynamics, high dimensionality and multiple delays.

Example 4

(Disease pathology [25, 27, 32]). Consider the following non-polynomial DDE for $t \ge 0$:

$$\begin{aligned} \dot{p}(t) = \frac{\beta \theta ^n p(t-r)}{\theta ^n + p^n(t-r)}-\gamma p(t), \end{aligned}$$

(24)

where p(t) is positive and indicates the number of mature blood cells in circulation, while r models the delay between cell production and cell maturation. We consider the case $\theta = 1$ as in [32]. Constants are instantiated as $n=1$, $\beta = 0.5$, $\gamma = 0.6$ and $r=0.5$. The unbounded verification problem of Eq. (24) over $[-r, \infty )$ is configured as $\mathcal {X}= [0, 0.2]$ and $\mathcal {U}= \{ p \mid \left|p\right| > 0.3 \}$. Then the linearization of Eq. (24) reads

$$\begin{aligned} \dot{p}(t) = - 0.6 p(t) + 0.5 p(t - 0.5). \end{aligned}$$

(25)

With $\alpha = -0.07$ obtained from DDE-BIFTOOL, our implementation produces for Eq. (25) the values $M=2.23562$, $K = 1.75081$, and thereby for Eq. (24) $\delta = 0.0163426$, $\tilde{K} = 0.0371712$ and $T^* = 0\,\hbox {s}$. Thereafter by the bounded verification method in [17], with Taylor models of the order 5, an overapproximation of the reachable set w.r.t. system (24) over the time interval [25.45, 25.95] was verified to be enclosed in the $\delta$-neighborhood of $\mathbf {0}$. This fact, together with $T^* = 0\,\hbox {s}$ and the overapproximation on $[-0.5, 25.95]$ being disjoint with $\mathcal {U}$, yields safety of the system (24) over $[-0.5, \infty )$.

Example 5

(Gene regulation [12, 36]). To examine the scalability of our technique to higher dimensions, we recall an instantiation of Eq. (2) by setting $n=5$, namely with 5 state components $\mathbf {x}= (x_1; \ldots ; x_5)$ and 5 delay terms $\mathbf {r}= (0.1; 0.2; 0.4; 0.8; 1.6)$ involved, $g(x) = -x$, $\beta _j = 1$ for $j = 1, \ldots , 5$, $\mathcal {X}= \mathcal {B}\left( \left( 1;1;1;1;1\right) , 0.2\right)$ and $\mathcal {U}=\{\mathbf {x}\mid \left|x_1\right| > 1.5\}$. With $\alpha = -0.04$ derived from DDE-BIFTOOL, our implementation returns $M = 64.264$, $K = 4.42207$, $\hat{K} = 49.1463$ and $T^* = 87.2334$ s, thereby yielding the equivalence of $\infty$-safety to T-safety for any $T > T^*$. Furthermore, the safety guarantee issued by the bounded verification method in [4] based on rigorous simulations under $T = 88$ s suffices to prove safety of the system over an infinite time horizon.

6 Conclusion

We have presented a constructive method, based on linearization and spectral analysis, for computing a delay-dependent, exponentially decreasing upper bound, if existent, that encloses trajectories of a DDE originating from a certain set of initial functions. We showed that such an enclosure facilitates a reduction of the verification problem over an unbounded temporal horizon to a bounded one. Preliminary experimental results on a set of representative benchmarks from the literature demonstrate that our technique effectively extends the scope of existing bounded verification techniques to unbounded verification tasks.

Peeking into future directions, we plan to exploit a tight integration of our technique into several automatic tools dedicated to bounded verification of DDEs, as well as more permissive forms of stabilities, e.g. asymptotical stability, that may admit a similar reduction-based idea. An extension of our method to deal with more general forms of DDEs, e.g., with time-varying, or distributed (i.e., a weighted average of) delays, will also be of interest. Additionally, we expect to refine our enclosure of system trajectories by resorting to a topologically finite partition of the initial set of functions.