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 safetycritical 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 delaydependent 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.
Keywords
Unbounded verification Delay Differential Equations (DDEs) Safety and stability Linearization Spectral analysis1 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 predatorprey 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, delayfree 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 finitedimensional states into an infinitedimensional dynamical system. There are approximation methods, say the Padé approximation [39], that approximate DDEs with finitedimensional 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 welldeveloped 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 stateexploratory 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 safetycritical 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( tr_1 \right) ,\ldots ,\mathbf {x}\left( tr_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 realworld 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 delaydependent, 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 discretecontinuous systems in a safetycritical context. The almost universal undecidability of the unbounded reachability problem, however, confines the sound keypress routines to either semidecision procedures or even approximation schemes, most of which address bounded verification by computing the finitetime image of a set of initial states. It should be obvious that the functional rather than statebased 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 propagationbased bounded verification: Huang et al. presented in [21] a technique for simulationbased timebounded 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 verificationbysimulation (see, e.g., [9, 16, 31]) was proposed in [4], which integrates rigorous error analysis of the numeric solving and the sensitivityrelated state bloating algorithms (cf. [7]) to obtain safe enclosures of timebounded 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 underapproximations 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 outerapproximating 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 delaydependent 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 timevarying and unknown timedelay 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\); \(\leftz\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 ith component, and its maximum norm is denoted by Open image in new window . We define for \(\delta > 0\), Open image in new window as the \(\delta \)closed ball around \(\mathbf {x}\). The notation Open image in new window extends to a set \(X \subseteq \mathbb {R}^n\) as Open image in new window , and to an \(m \times n\) complexvalued matrix A as Open image in new window . \({}\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 Open image in new window . 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 Open image in new window 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\).
Suppose \({\varvec{f}}\) is a Lipschitzcontinuous vectorvalued 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 Open image in new window the Jacobian matrix (i.e., matrix consisting of all firstorder partial derivatives) of \({\varvec{f}}\) w.r.t. the component \(\mathbf {x}\left( t\right) \). Similar notations apply to components \(\mathbf {x}\left( tr_i \right) \), for \(i = 1, \ldots , k\).
Example 1

\(\mathbf {x}_e\) is said to be Lyapunov stable, if for every \(\epsilon > 0\), there exists \(\delta > 0\) such that, if Open image in new window , then for every \(t \ge 0\) we have Open image in new window .

\(\mathbf {x}_e\) is said to be asymptotically stable, if it is Lyapunov stable and there exists \(\delta > 0\) such that, if Open image in new window , then Open image in new window .

\(\mathbf {x}_e\) is said to be exponentially stable, if it is asymptotically stable and there exist \(\alpha ,\beta ,\delta > 0\) such that, if Open image in new window , then Open image in new window , 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 Open image in new window 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
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 infinitedimensional 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
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 socalled 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
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 wellknown method of steps [8].
Lemma 3
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
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 nontrivial 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 LMSmethods. A welldeveloped Matlab package called DDEBIFTOOL [10] is furthermore available to mechanize the computation, which will be demonstrated in our forthcoming examples.
3.2 Constructing K
Lemma 4
Proof
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
Proof
The “only if” part is for free, as \(\infty \)safety subsumes by definition Tsafety. For the “if” direction, the constructed K in Eq. (12) suffices as an upper bound of Open image in new window , and hence by Theorem 2, Open image in new window 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^{3} of \(T^*\), which further implies \(T^* < \infty \). \(\square \)
Example 2
\([\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 Tsafety 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].
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.
In light of the wellknown HartmanGrobman 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
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
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
Proof
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
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 Open image in new window , due to the locality stemming from linearization. In fact, such a set \(\mathfrak {B}\subseteq \mathbb {R}^n\) satisfying Open image in new window 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 Tsafe. This is furthermore demonstrated by the following example.
Example 3
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 Open image in new window with Open image in new window and Open image in new window with Open image in new window , where \(A_i\) denotes the matrix attached to \(\mathbf {x}(t  r_i)\) in the linearization. For a slightly modified form of the variationofconstants 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^{4} in Wolfram Mathematica, which was selected due to its builtin primitives for integration and matrix operations. By interfacing with DDEBIFTOOL^{5} (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 Corei7 processor with 8 GB RAM running 64bit 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 nonpolynomial dynamics, high dimensionality and multiple delays.
Example 4
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 \leftx_1\right > 1.5\}\). With \(\alpha = 0.04\) derived from DDEBIFTOOL, 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 Tsafety 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 delaydependent, 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 reductionbased idea. An extension of our method to deal with more general forms of DDEs, e.g., with timevarying, 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.
Footnotes
References
 1.Bellman, R.: The stability of solutions of linear differential equations. Duke Math. J. 10(4), 643–647 (1943)MathSciNetCrossRefGoogle Scholar
 2.Bellman, R.E., Cooke, K.L.: Differentialdifference equations. Technical Report R374PR, RAND Corporation, Santa Monica, California, January 1963Google Scholar
 3.Breda, D., Maset, S., Vermiglio, R.: Computing the characteristic roots for delay differential equations. IMA J. Numer. Anal. 24(1), 1–19 (2004)MathSciNetCrossRefGoogle Scholar
 4.Chen, M., Fränzle, M., Li, Y., Mosaad, P.N., Zhan, N.: Validated simulationbased verification of delayed differential dynamics. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 137–154. Springer, Cham (2016). https://doi.org/10.1007/9783319489896_9CrossRefGoogle Scholar
 5.Cooke, K.L.: Stability analysis for a vector disease model. Rocky Mt. J. Math. 9(1), 31–42 (1979)MathSciNetCrossRefGoogle Scholar
 6.Diekmann, O., van Gils, S., Lunel, S., Walther, H.: Delay Equations: Functional, Complex, and Nonlinear Analysis. Applied Mathematical Sciences. Springer, New York (2012). https://doi.org/10.1007/9781461242062CrossRefGoogle Scholar
 7.Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540714934_16CrossRefGoogle Scholar
 8.Driver, R.: Ordinary and Delay Differential Equations. Applied Mathematical Sciences. Springer, New York (1977). https://doi.org/10.1007/9781468494679CrossRefzbMATHGoogle Scholar
 9.Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: EMSOFT 2013, pp. 26:1–26:10 (2013)Google Scholar
 10.Engelborghs, K., Luzyanina, T., Roose, D.: Numerical bifurcation analysis of delay differential equations using DDEBIFTOOL. ACM Trans. Math. Softw. 28(1), 1–21 (2002)MathSciNetCrossRefGoogle Scholar
 11.Engelborghs, K., Roose, D.: On stability of LMS methods and characteristic roots of delay differential equations. SIAM J. Numer. Anal. 40(2), 629–650 (2002)MathSciNetCrossRefGoogle Scholar
 12.Fall, C.P., Marland, E.S., Wagner, J.M., Tyson, J.J. (eds.): Computational Cell Biology, vol. 20. Springer, New York (2002)zbMATHGoogle Scholar
 13.Fort, J., Méndez, V.: Timedelayed theory of the neolithic transition in Europe. Phys. Rev. Lett. 82(4), 867 (1999)CrossRefGoogle Scholar
 14.Fränzle, M., Chen, M., Kröger, P.: In memory of Oded Maler: automatic reachability analysis of hybridstate automata. ACM SIGLOG News 6(1), 19–39 (2019)Google Scholar
 15.Gan, T., Chen, M., Li, Y., Xia, B., Zhan, N.: Reachability analysis for solvable dynamical systems. IEEE Trans. Automat. Contr. 63(7), 2003–2018 (2018)MathSciNetCrossRefGoogle Scholar
 16.Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5–6), 568–578 (2011)MathSciNetCrossRefGoogle Scholar
 17.Goubault, E., Putot, S., Sahlmann, L.: Inner and outer approximating flowpipes for delay differential equations. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 523–541. Springer, Cham (2018). https://doi.org/10.1007/9783319961422_31CrossRefGoogle Scholar
 18.Grobman, D.M.: Homeomorphism of systems of differential equations. Doklady Akademii Nauk SSSR 128(5), 880–881 (1959)MathSciNetzbMATHGoogle Scholar
 19.Hale, J., Lunel, S.: Introduction to Functional Differential Equations. Applied Mathematical Sciences. Springer, New York (1993). https://doi.org/10.1007/9781461243427CrossRefzbMATHGoogle Scholar
 20.Hartman, P.: A lemma in the theory of structural stability of differential equations. Proc. Am. Math. Soc. 11(4), 610–620 (1960)MathSciNetCrossRefGoogle Scholar
 21.Huang, Z., Fan, C., Mitra, S.: Bounded invariant verification for timedelayed nonlinear networked dynamical systems. Nonlinear Anal. Hybrid Syst. 23, 211–229 (2017)MathSciNetCrossRefGoogle Scholar
 22.Hutchinson, G.E.: Circular causal systems in ecology. Ann. N. Y. Acad. Sci. 50(4), 221–246 (1948)CrossRefGoogle Scholar
 23.Ikeda, K., Matsumoto, K.: Highdimensional chaotic behavior in systems with timedelayed feedback. Phys. D Nonlinear Phenom. 29(1–2), 223–235 (1987)CrossRefGoogle Scholar
 24.Krasovskiĭ, N.: Stability of Motion: Applications of Lyapunov’s Second Method to Differential Systems and Equations with Delay. Studies in Mathematical Analysis and Related Topics. Stanford University Press, Stanford (1963)zbMATHGoogle Scholar
 25.Kuang, Y.: Delay Differential Equations: With Applications in Population Dynamics. Mathematics in Science and Engineering. Elsevier Science, Amsterdam (1993)zbMATHGoogle Scholar
 26.Levine, W.S.: The Control Handbook: Control System Fundamentals. Electrical Engineering Handbook, 2nd edn. CRC Press, Boca Raton (2010)Google Scholar
 27.Mackey, M.C., Glass, L.: Oscillation and chaos in physiological control systems. Science 197(4300), 287–289 (1977)CrossRefGoogle Scholar
 28.MalletParet, J., Sell, G.R.: The PoincaréBendixson theorem for monotone cyclic feedback systems with delay. J. Differ. Equ. 125, 441–489 (1996)CrossRefGoogle Scholar
 29.Nazier Mosaad, P., Fränzle, M., Xue, B.: Temporal logic verification for delay differential equations. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 405–421. Springer, Cham (2016). https://doi.org/10.1007/9783319467504_23CrossRefGoogle Scholar
 30.Myshkis, A.D.: Lineare Differentialgleichungen mit nacheilendem Argument, vol. 17. VEB Deutscher Verlag der Wissenschaften (1955)Google Scholar
 31.Nahhal, T., Dang, T.: Test coverage for continuous and hybrid systems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 449–462. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540733683_47CrossRefGoogle Scholar
 32.Peet, M., Lall, S.: Constructing Lyapunov functions for nonlinear delaydifferential equations using semidefinite programming. In: Proceedings of NOLCOS, pp. 381–385 (2004)Google Scholar
 33.Pola, G., Pepe, P., Benedetto, M.D.D.: Symbolic models for timevarying timedelay systems via alternating approximate bisimulation. Int. J. Robust Nonlinear Control 25, 2328–2347 (2015)MathSciNetCrossRefGoogle Scholar
 34.Pola, G., Pepe, P., Benedetto, M.D.D., Tabuada, P.: Symbolic models for nonlinear timedelay systems using approximate bisimulations. Syst. Control Lett. 59(6), 365–373 (2010)MathSciNetCrossRefGoogle Scholar
 35.Prajna, S., Jadbabaie, A.: Methods for safety verification of timedelay systems. In: CDC 2005, pp. 4348–4353 (2005)Google Scholar
 36.Smith, H.: An Introduction to Delay Differential Equations with Applications to the Life Sciences, vol. 57. Springer, New York (2011). https://doi.org/10.1007/9781441976468CrossRefzbMATHGoogle Scholar
 37.Strzeboński, A.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46(11), 1284–1290 (2011)MathSciNetCrossRefGoogle Scholar
 38.Szydłowski, M., Krawiec, A., Toboła, J.: Nonlinear oscillations in business cycle model with time lags. Chaos Solitons Fractals 12(3), 505–517 (2001)CrossRefGoogle Scholar
 39.Vajta, M.: Some remarks on padéapproximations. In: Proceedings of the 3rd TEMPUSINTCOM Symposium, vol. 242 (2000)Google Scholar
 40.van den Berg, J.B., Jaquette, J.: A proof of Wright’s conjecture. J. Differ. Equ. 264(12), 7412–7462 (2018)MathSciNetCrossRefGoogle Scholar
 41.Volterra, V.: Une théorie mathématique de la lutte pour la vie (1927)Google Scholar
 42.Volterra, V.: Sur la théorie mathématique des phénomenes héréditaires. Journal de mathématiques pures et appliquées 7, 249–298 (1928)zbMATHGoogle Scholar
 43.Vyhlídal, T.: Analysis and synthesis of time delay system spectrum. Ph.D. dissertation, Czech Technical University in Prague (2003)Google Scholar
 44.Wright, E.M.: A nonlinear differencedifferential equation. J. Reine Angew. Math. 66–87, 1955 (1955)MathSciNetGoogle Scholar
 45.Wulf, V., Ford, N.J.: Numerical hopf bifurcation for a class of delay differential equations. J. Comput. Appl. Math. 115(1–2), 601–616 (2000)MathSciNetCrossRefGoogle Scholar
 46.Xue, B., Mosaad, P.N., Fränzle, M., Chen, M., Li, Y., Zhan, N.: Safe over and underapproximation of reachable sets for delay differential equations. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 281–299. Springer, Cham (2017). https://doi.org/10.1007/9783319657653_16CrossRefzbMATHGoogle Scholar
 47.Zou, L., Fränzle, M., Zhan, N., Mosaad, P.N.: Automatic verification of stability and safety for delay differential equations. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 338–355. Springer, Cham (2015). https://doi.org/10.1007/9783319216683_20CrossRefzbMATHGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.