Validated Simulation-Based Verification of Delayed Differential Dynamics

Abstract

Verification by simulation, based on covering the set of time-bounded trajectories of a dynamical system evolving from the initial state set by means of a finite sample of initial states plus a sensitivity argument, has recently attracted interest due to the availability of powerful simulators for rich classes of dynamical systems. System models addressed by such techniques involve ordinary differential equations (ODEs) and can readily be extended to delay differential equations (DDEs). In doing so, the lack of validated solvers for DDEs, however, enforces the use of numeric approximations such that the resulting verification procedures would have to resort to (rather strong) assumptions on numerical accuracy of the underlying simulators, which lack formal validation or proof. In this paper, we pursue a closer integration of the numeric solving and the sensitivity-related state bloating algorithms underlying verification by simulation, together yielding a safe enclosure algorithm for DDEs suitable for use in automated formal verification. The key ingredient is an on-the-fly computation of piecewise linear, local error bounds by nonlinear optimization, with the error bounds uniformly covering sensitivity information concerning initial states as well as integration error.

The first, third and fifth authors are supported partly by “973 Program” under grant No. 2014CB340701, by NSFC under grants 91418204 and 61502467, by CDZ project CAP (GZ 1023), and by the CAS/SAFEA International Partnership Program for Creative Research Teams. The second and fourth authors are supported partly by Deutsche Forschungsgemeinschaft within the Research Training Group “SCARE - System Correctness under Adverse Conditions” (DFG GRK 1765).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Delayed coupling between state variables of dynamic systems occurs in many domains. Prominent examples include population dynamics, where birth rate follows changes in population size with a delay related to reproductive age, spreading of infectious diseases, where delay is induced by the incubation period, exhaust gas control in internal combustion engines, where relevant sensors, like the $\lambda$ probe, are located downstream the exhaust system such that gas transport induces a delay between the controlled combustion processes and sensing their effect, or networked control systems with their associated transport delays when forwarding data through the communication network, to name just a few. Most examples feature feedback dynamics and it should be obvious that the presence of feedback delays reduces controllability due to the impossibility of immediate reaction and enhances likelihood of transient overshoot or even oscillation in the feedback system. In fact, the introduction of delays into a feedback system may reduce stabilization rates of or even destabilize an otherwise stable system, it may provoke overshoot and drive the system to otherwise unreachable states, it is likely to stretch dwell times, and it may induce residual error that never cancels. As this implies that safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling may be erratic, automated methods for system verification ought to address models of system dynamics reflecting delays, rendering verification tools only addressing ordinary differential equations (ODE) and their derived models, like hybrid automata, vastly insufficient. It can well be argued that such tools should better address delay differential equations (DDE), as introduced in [2].

Generalizing techniques developed for ODE to DDE is not as straightforward as it may seem at first glance. 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 past trajectory, such that introducing a delay immediately renders a system with finite-dimensional state into an infinite-dimensional dynamical system. Consequently, approximate numerical methods for solving DDEs as well as methods for stability analysis have well been developed in the field of control, while in automatic verification, hitherto only 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 address this problem by suitably adapting the paradigm of verification by simulation to delay differential equations. Verification by simulation provides bounded-time verification of dynamical systems based on covering the full set of time-bounded trajectories of a dynamical system evolving from the initial state set by means of a finite sample of initial states plus a sensitivity argument. To achieve this, a sufficiently dense sample of initial states is drawn from the set of all possible initial states, numeric simulation is then used for obtaining the trajectories originating from the sample points, and finally a quantitative sensitivity argument permits to pessimistically over-approximate the “tube” of trajectories originating from arbitrary start states by means of “bloating” the individual simulated trajectories into a neighborhood of the radius given by the bound on sensitivity on the start state, see e.g. [8, 9, 15, 20]. If a validated numerical solver is used for the simulations, the above procedure will immediately yield a safe over-approximation of the set of possible trajectories; else, more aggressive bloating additionally covering the possible inaccuracies of numeric integration of differential equations has to be employed to obtain a sound, validated method.

The class of systems we approach features delayed differential dynamics governed by DDE of the following form:

$$\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{g}(t), \quad t \in \left[ -r_\mathrm{max},0 \right] \end{array} \right. \end{aligned}$$

(1)

It thus involves a combination of ODE and DDE with multiple constant delays $r_i > 0, i=1,\ldots ,k$. Here, $r_\mathrm{max}=\mathrm{max}\{r_1,\ldots ,r_k\}$ is the maximal delay, $\mathbf {x}:\mathbb {R}_{\ge -r_\mathrm{max}} \mapsto \mathbb {R}^n$ is a trajectory, $\varvec{f}:(\mathbb {R}^n)^{k+1} \mapsto \mathbb {R}^n$ a vector field, and $\varvec{g}:[-r_\mathrm{max},0] \mapsto \mathbb {R}^n$ is a continuous function providing the initial condition. This form of equations has been successfully used to model various real world systems in the fields of, e.g., biology, control theory, and economics.

Generally speaking, formal verification of temporally unbounded reachability properties of system dynamics governed by Eq. (1) inherits undecidability from similar properties for ODE. Therefore, and also due to our wish to use simulation as an underlying mechanism of system analysis, we restrict ourselves to time-bounded reachability problems. Such a time-bounded reachability problem for a given model of the form (1) is parameterized by a temporal horizon (i.e., a time bound) set by the user, a set of initial states which in the case of DDE generalizes to constant functions over the time frame $[-r_\mathrm{max},0]$ immediately preceding system start, and a set of unsafe states that system dynamics is expected to avoid. The proof obligation is to determine whether there exists a trajectory of the model starting in some initial state which reaches any unsafe state within the time bound. In our approach, we first trigger a set of numerical approximations of the behaviours from a finite sampling of the initial states. Such a simulation does not yield a trajectory, but rather a timed trace, i.e., a sequence of time-stamp value pairs. Along each simulation run, we bloat each snapshot, i.e., each time-stamp value pair by a distance determined via an error bound computed automatically on-the-fly, where the error bound incorporates coverage and sensitivity information concerning the sampled start states as well as the integration error incurred by numerical solving. The union of these bloatings covers all time-bounded trajectories possibly evolving from all initial states, and thus yields an over-approximation of the states reachable from the initial set within the time bound. If this over-approximation proves safety in the sense that the cover of the reachable states is disjoint from the unsafe states, or conversely if the simulation produces a valid counter-example in the sense that it can prove that a trajectory inevitably hits the unsafe states, then the algorithm generates the corresponding verdict. Otherwise, it refines the sample drawn from the initial states, thus requiring less aggressive bloating of simulation runs, and computes a more precise over-approximation.

Our approach is distinguished from competing approaches by providing a validated verification-by-simulation paradigm for DDE. Given that validated methods for DDE enclosure are not readily available, it achieves this by pursuing a closer than traditional integration of the numeric solving and the sensitivity-related state bloating algorithms underlying verification by simulation, together yielding a safe enclosure algorithm for DDE guaranteed to contain the true solution. The key ingredient is an on-the-fly computation of piecewise linear, local error bounds by nonlinear optimization, which provides an alternative to established methods computing discrepancy bounds from Lipschitz constants and Jacobians, as employed in [13]. Some experimental results obtained on several benchmark systems involving delayed differential dynamics are further demonstrated. Due to lack of space, the detailed proofs of theorems are available in [5].

Related Work. Zou et al. proposed in [27] a procedure for generating stability and safety certificates for the simplest class of DDEs of the form $\dot{\mathbf {x}}(t) = \varvec{f}(\mathbf {x}(t-r))$. This is achieved by iterating interval-based Taylor over-approximations of the time-wise segments of the solution to a DDE, which depends essentially on the fact that the interval coefficients of the solution over the time interval $(n,n+1]$ can be represented as a function of those of the solution over $(n-1,n]$. Extracting the operator mapping coefficients at one time frame to those of the next, one obtains a time-invariant discrete-time dynamical system. Thus, stability analysis and safety verification of the original DDE is reduced to appropriate counterparts encoding these properties on the resulting time-invariant discrete-time dynamical system. This approach does not immediately generalize to mixed ODE-DDE forms as in Eq. (1), as the delayed parts of the dynamics would there function as inputs to an ODE with input, rendering the above operator time-variant. Though this is doable in principle, we have herein opted for the more immediate approach of verification by simulation.

In [22], Pola et al. proposed an approach abstracting incrementally input-to-state stable ($\delta$-ISS) nonlinear control systems with constant and known delays to finite-state symbolic models, and establish approximate bisimilarity between them. In [21], they extended the work in [22] to incrementally-input-delay-to-state stable ($\delta$-IDSS) nonlinear control systems with time-varying and unknown delays, and proved that the original $\delta$-IDSS nonlinear control systems and the corresponding symbolic models are alternating approximately bisimilar. The crucial differences between their work and ours lie in, firstly, their approach being confined to $\delta$-ISS nonlinear control systems, while our approach being applicable to any kind of nonlinear control systems with constant and known time delays. So, our method relaxes a problematic applicability condition. Second, their approach can do unbounded verification of time-delay systems, while our approach currently can only conduct bounded verification. Third, their approach can be applied to $\delta$-IDSS nonlinear control systems with time-varying and unknown delays, while our approach cannot yet. It is a crucial aspect of our future work to extend our approach to nonlinear control systems with time-varying and unknown delays, without sacrificing its applicability beyond $\delta$-IDSS systems.

Verifying delayless dynamical systems, in particular ODE, using numerical simulations has well been studied, e.g., in [8, 9, 15, 20], where similar concepts based on sensitivity information provided by discrepancy functions or simulation functions, respectively, have been presented to bloat the traces obtained from simulations to “trajectory tubes” over-approximating time-bounded reach sets. While the first settings resorted to user-supplied sensitivity information, Fan and Mitra in [13] proposed an algorithm for automatically computing piecewise exponential discrepancy functions. This algorithm pessimistically estimates the sensitivity of the ODE on its initial value, but also takes assumed error bounds of the numerical simulation, which in that case is Matlab’s ode45 solver, into account. This, however, renders the soundness of this algorithm dependent on the assumption that Matlab’s built-in ODE solver can always guarantee those numerical error bounds, while it is possible to find extremely stiff ODEs as follows for which the solver returns very inaccurate results.

$$\begin{aligned} \dot{x} (t) = 1 + \delta _a(x-\sqrt{2}), \text { with } \delta _a(y) = \frac{1}{a\sqrt{\pi }}\mathrm {e}^{-y^2/a^2} \end{aligned}$$

(2)

$\delta _a(y)$ approximates the Dirac $\delta$ function [7] modelling a tall narrow spike around $y = 0$, where the spike shrinks as $a \rightarrow 0$. When Eq. (2) is simulated with $a = 10^{-3}$ by Matlab’s ODE solver ode45, results show that the solver can detect the sharp increment of the derivative with a user-specified MaxStep as 0.01, while not the case with 0.1. Furthermore, adjusting the simulation step width could not essentially cure the problem, yet just shifts it to a smaller a for which the solver fails to identify the leaping trajectory and instead follows straight-line dynamics. This motivates us to address the issue of numerical errors in discrepancy computation. Moreover, the method in [13] requires computations of a global Lipschitz constant as well as a bound on the eigenvalues of the Jacobians within a region, which may not be feasible in some dynamical systems.

2 Problem Formulation

Notations. For a vector $\mathbf {x}\in \mathbb {R}^n$, $x_i$ refers to its $i\mathrm{th}$ component, and $\Vert \mathbf {x}\Vert$ denotes the $\ell ^2$-norm. The notation $\Vert \cdot \Vert$ extends to an $n \times n$ real matrix $A \in \mathbb {R}^{n \times n}$ with $\Vert A\Vert = \sqrt{\lambda _\mathrm{max}(A^\mathrm{T}A)}$, where $\lambda _\mathrm{max}(A)$ is the largest eigenvalue of A. For $\mathbf {x},\mathbf {x}' \in \mathbb {R}^n$, $\Vert \mathbf {x}' - \mathbf {x}\Vert$ is the Euclidean distance between the points, and we define for $\delta \ge 0$, $\mathcal {B}_\delta (\mathbf {x}) = \{\mathbf {x}' \in \mathbb {R}^n | \Vert \mathbf {x}'-\mathbf {x}\Vert \le \delta \}$ as the closed ball of radius $\delta$ centered at $\mathbf {x}$. For a set $S \subseteq \mathbb {R}^n$, $\mathcal {B}_\delta (S) = \cup _{\mathbf {x}\in S}\mathcal {B}_\delta (\mathbf {x})$. The diameter of a compact set S is $\textit{dia}(S) = \sup _{\mathbf {x},\mathbf {x}' \in S}\Vert \mathbf {x}- \mathbf {x}'\Vert$, and a $\delta$-cover of S is a finite collection of points $\mathcal {X}$ such that $S \subseteq \cup _{\mathbf {x}\in \mathcal {X}} \mathcal {B}_\delta (\mathbf {x})$. For a set $S \subseteq \mathbb {R}^n$, its convex hull is denoted as $\textit{conv}(S)$.

Delayed Dynamical Systems. We consider a timed-bounded delayed dynamical system of the form

$$\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) &{}\equiv \mathbf {x}_0 \in \varTheta , \quad t \in \left[ -r_k,0 \right] , \end{array} \right. \end{aligned}$$

(3)

¹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 generalized to a constant function over $[-r_k,0]$ taking values from a compact set $\varTheta$.

Let the vector-valued function $\varvec{f}: (\mathbb {R}^n)^{k+1} \mapsto \mathbb {R}^n$ be continuous and continuously differentiable in the first argument, which implies that the system has a unique maximal solution (or trajectory) from each constant initial condition valued $\mathbf {x}_0\in \mathbb {R}^n$, denoted as $\mathbf {\xi }_{\mathbf {x}_0}(t): [-r_k,\ell ) \mapsto \mathbb {R}^n$, where $\ell =\infty$ holds if $\varvec{f}$ is Lipschitz.

Example 1

(Gene Regulation [12, 24]). 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(x_n(t-r_n)) - \alpha _1 x_1(t) \\ \dot{x_j}(t) &{}= g(x_{j-1}(t-r_{j-1})) - \alpha _j x_j(t), 1 < j \le n, \end{array} \right. \end{aligned}$$

(4)

where the gene is transcribed producing mRNA ($x_1$), which is translated into enzyme $x_2$ that 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 $\alpha _j > 0$ represent decay rates of the species. The dynamic described in Eq. (4) 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) [19], which includes neural networks, testosterone control, and many other effects in systems biology.

Safety Verification Problem. Given a set $\mathcal {U}\subseteq \mathbb {R}^n$ of unsafe or otherwise bad states, a delayed dynamical system of shape (3) is said to be (time-bounded) safe iff all the trajectories originating from any $\mathbf {x}_0 \in \varTheta$ do not intersect with $\mathcal {U}$ (within the given time bound T), otherwise it is called unsafe.

3 Verification of Delayed Dynamical Systems via Simulation

Generating formal guarantees for DDEs of the form (3) tends to be challenging due to unavailability of guaranteed for solving them. We are trying to alleviate that problem by adopting approximate numeric methods, enhancing them with methods for rigorous error tracking, thus rendering them validated numerical methods, and adding sensitivity information for being able to cover sets of initial states based on simulating and bloating the trajectories originating from finitely many samples. This approach has been inspired by similar approaches for ODE, in particular the discrepancy functions of [13].

We will now expose in detail the overall procedure of simulation by verification, which hinges on the validated simulation of DDE that we will turn to in Sect. 4. For the sake of simplifying the exposition, we first consider the special case of delayed dynamical systems featuring a single delay, as in

$$\begin{aligned} \left\{ \begin{array}{lll} \dot{\mathbf {x}} \left( t \right) &{}= \varvec{f}\left( \mathbf {x}\left( t \right) ,\mathbf {x}\left( t-r\right) \right) , &{} ~~t\in [0,\infty ) \\ \mathbf {x}\left( t \right) &{}\equiv \mathbf {x}_0 \in \varTheta , &{} ~~ t \in \left[ -r,0 \right] . \end{array} \right. \end{aligned}$$

(5)

In this case, the differential dynamics is a function $\varvec{f}(\mathbf {x}, \mathbf {u})$ of two states, namely the current state $\mathbf {x}$ and the past state $\mathbf {u}$.

The basic idea of simulation-based verification of a DDE (5), as implemented by Algorithm 1, can be sketched as follows:

First, we build on a validated simulation procedure $\text {Simulation}$, whose design is shown in Sect. 4. Given a delayed dynamical system as above, a subset $\mathcal{X}_0 \subset \varTheta$ of the initial states, and a time bound T, $\text {Simulation}$ yields a simulation trace $(t_0,\mathbf {y}_0),\ldots , (t_n, \mathbf {y}_n)$ consisting of pairs of time stamps $t_i\in [0,T]$ and states $\mathbf {y}_i\in \mathbb {R}^n$ with $\mathbf {y}_0 = \mathbf {x}_0$, as well as a sequence of local error bounds $d_0,d_1,\ldots , d_n \ge 0$ providing a validation of this trace observing the following two properties:

• P1: $0=t_0<t_1<\ldots <t_n=T$, i.e., the time stamps in the trace are ascending and cover the temporal horizon of interest.

• P2: For each of the trajectories $\mathbf {\xi }_{\mathbf {x}_0}(t)$ of (5) starting from any point $\mathbf {x}_0\in \mathcal{X}_0$, the validation property

  $$\begin{aligned} (\mathbf {\xi }_{\mathbf {x}_0}(t),t) \in \textit{conv}\left( \begin{array}{l} (\mathcal {B}_{\mathbf {d}_i}(\mathbf {y}_i)\times \{t_i\}) \cup (\mathcal {B}_{\mathbf {d}_{i+1}}(\mathbf {y}_{i+1})\times \{t_{i+1}\}) \end{array} \right) \end{aligned}$$

  (6)

  holds for each $t\in [t_i,t_{i+1}]$, $i = 0,1, \ldots , n-1$. I.e., the reported error bounds $\mathbf {d}_i$ span a piecewise linear tube around the points $(\mathbf {y}_i,t_i)$ in the simulation trace such that $\mathbf {\xi }_{\mathbf {x}_0}(t)$ is properly enclosed for any $\mathbf {x}_0\in \mathcal{X}_0$ and any $t\in [0,T]$.

Then, time-bounded safety verification of system (5) can be obtained as follows:

• 1. At the beginning, we cover the given initial set $\mathcal {X}_0$ by a finite set of balls of radius $\delta$; so, $\delta \text {-Partition}(\mathcal {X}_0)$ in line 2 of Algorithm 1 returns a finite $\delta \text {-cover}$ of the compact set $\mathcal {X}_0$. We then call $\text {Simulation}$ to each of these balls. For each ball B, we collect all states contained in the bloating of the N-step simulation trace $\mathbf {y}$ as $\mathcal {B}_{\mathbf {d}}(\mathbf {y}) = \bigcup \nolimits _{n=0}^{N-1} \textit{conv}(\mathcal {B}_{\mathbf {d}_n}(\mathbf {y}_n)\cup \mathcal {B}_{\mathbf {d}_{n+1}}(\mathbf {y}_{n+1}))$, cf. line 8. This yields an over-approximation of the states reachable from B following (5) within time up to T.

• 2. If the over-approximation of the reachable set thus obtained is disjoint to the unsafe set (line 9), then (5) is safe when starting in B; otherwise, if there exists a sampling point in the simulation which has its full bloating with the corresponding local error bound being contained in the unsafe set (line 11), then (5) is definitely unsafe. If none of these two conditions applies, we compute a finer partition of B (line 14), and we repeat the above procedure until the granularity of the partition becomes finer than the given threshold. In this case, we cannot give an answer whether or not (5) is safe and terminate with the inconclusive result unknown.

Obviously, our approach is different from existing approaches providing simulation-based verification for dynamical systems modeled by ordinary differential equations, like [8, 9]. In our approach, the simulation procedure provides a rigorous validation of the above property P2, rather than relying on assumptions concerning numerical accuracy of the underlying simulator. Second, our approach covers rigorous simulation-based formal verification of DDE rather than just ODE. The correctness of the resulting algorithm is captured by the following theorem:

Theorem 1

(Correctness). If Simulation satisfies above properties P1 and P2 (which will be verified in the next section), then Algorithm 1 terminates and its outputs are guaranteed to satisfy the following soundness properties:

• it reports (SAFE,$\mathcal {R}$) only if the system is safe.

• it reports (UNSAFE, $\mathcal {T}$) only if the system is unsafe and $\mathcal {T}$ is a counter-example.

The general case of multiple different delays in Eq. (3) can be dealt with analogously to the case (5) of a single delay: we only need to allow $\mathbf {u}$ to have more components, meanwhile, we need to revise Algorithm 2 accordingly by introducing multiple different $m_i$ as $m_1 \leftarrow r_1/\tau ,\ldots ,m_k \leftarrow r_k/\tau$. Thus, the delayed states $y_{n-m_i}$s can be exactly located when computing $y_{n+1}$ by $\varvec{f}(y_n,y_{n-m_1},\ldots ,y_{n-m_k})$ (line 6 in Algorithm 2) as well as when finding the minimal e (line 7 in Algorithm 2).

4 Validated Simulation

In this section, we elaborate on simulation and on computation of rigorous local error bounds to guarantee the enclosure property P2. Instead of directly computing the error bounds $d_0,\ldots ,d_n$ accompanying the simulation trace $(t_0,\mathbf {y}_0),\ldots ,(t_n,\mathbf {y}_n)$, we compute an initial error bound $d_0$ and a sequence $e_1,\ldots ,e_n$ of error slopes recursively defining error bounds E(t) for each $t\in [0,T]$ — and thus not only for time stamps in the simulated trace — as follows:

$$\begin{aligned} E(t) = {\left\{ \begin{array}{ll} d_0, &{} \text { if } \ t=0,\\ E(t_i) + (t-t_i) e_{i+1},&{} \text { if }\ t\in [t_i,t_{i+1}]. \end{array}\right. } \end{aligned}$$

(7)

The validation property (P2) can thus be rewritten as

• P2’: For each of the trajectories $\mathbf {\xi }_{\mathbf {x}_0}(t)$ of system (5) starting from any point $\mathbf {x}_0\in \mathcal{X}_0$, the validation property

  $$\begin{aligned} \mathbf {\xi }_{\mathbf {x}_0}(t) \in \mathcal {B}_{E(t)}\left( \frac{(t-t_i)\mathbf {y}_i+(t_{i+1}-t)\mathbf {y}_{i+1}}{t_{i+1}-t_i}\right) \end{aligned}$$

  (8)

  holds for each $t\in [t_i,t_{i+1}]$.

I.e., the $e_i$’s provide the slopes of piecewise conic enclosures around the linear interpolations between the points $(t_i,\mathbf {y}_i)$ in the simulation trace.

The Simulation Algorithm. Inferring formal proofs from simulations essentially attributes to a validated numerical solver which can produce rigorous error bounds on the generated sampling points. We present in Algorithm 2 a procedure² Simulation that provides a trace of sampling points bundled with their local error bounds thus giving an over-approximation of the reachable set in terms of an initial state space.

The algorithm is provided with an initial ball $\mathcal {B}_\delta (\mathbf {x}_0)$ and it proceeds with a discrete simulation starting from $\mathbf {x}_0$ paced by a fixed stepsize $\tau$. Three list structures (denoted as $\llbracket \cdot \rrbracket$) with the same length are introduced respectively as (1) $\mathbf {t}$: storing a sequence of time stamps on which the approximations are computed, (2) $\mathbf {y}$: keeping a sequence of sampling points that approximates the trajectory starting from $\mathbf {x}_0$, and (3) $\mathbf {d}$: capturing the corresponding sequence of local error bounds. Due to the nature of DDEs where the evolving of states may refer to those ahead of time $t_0 = 0$, we index the lists beginning from $-1$ and assume that all the evaluations of $\mathbf {y}$ and $\mathbf {d}$ with a negative index return the element at $-1$, namely $\mathbf {y}_{<0} = \mathbf {y}_{-1}$ ³, and analogously for $\mathbf {d}$.

At $t_0 = 0$, the corresponding local error is initialized with the radius of the initial set $d_0 = \delta$ (line 1). An offest m is computed in line 2 such that $\mathbf {y}_{n-m}$ locates the delayed approximation at $t_n-r$. In each iteration of the simulation loop, the state is extrapolated in line 6 using the well-known forward Euler method, which computes $y_{n+1}$ explicitly from previous points $y_n$ and $y_{n-m}$. Higher-order Runge-Kutta methods [1] could be employed here to obtain more precise approximations. Line 7 derives a local error bound $d_{n+1}$ based on the local error slope $e_n$ satisfying the enclosure property (P2’). The computation of $e_n$ is reduced to a constrained optimization problem (line 6).

Correctness of Simulation. Note that the constrained optimization problem (9) need not have a finite solution, in which case our algorithm fails to provide a useful enclosure. Straightforward continuity arguments do, however, show that for small enough stepsize $\tau$, it will always have a solution, which motivated us to implement stepsize control, as discussed below. When being able to compute useful, i.e., finite error slopes, the simulation delivers a safe enclosure satisfying (P2):

Theorem 2

(Correctness). Suppose the maximum index of the lists generated by Algorithm 2 is N, then $\forall t \in [0,T]$ and $\forall \mathbf {x}\in \mathcal {B}_\delta (\mathbf {x}_0)$,

$$\begin{aligned} \mathbf {\xi }_{\mathbf {x}}(t) \subseteq \bigcup \nolimits _{n=0}^{N-1} \textit{conv}(\mathcal {B}_{\mathbf {d}_n}(\mathbf {y}_n)\cup \mathcal {B}_{\mathbf {d}_{n+1}}(\mathbf {y}_{n+1})). \end{aligned}$$

The completeness result can be formally stated as follows:

Theorem 3

(Completeness). Suppose the function $\varvec{f}$ in Eq. (5) is continuously differentiable in both arguments and the dynamical system is solvable for time interval [0, T], then for any $\varepsilon >0$, there exists $\delta$, $\tau$ and $\sigma$ such that the optimization problem (9) has a solution $e_n$ for all $n\le \frac{T}{\tau }$, and moreover $\mathbf {d}_n\le \varepsilon$.

Extension to Variable Stepsize. Local stepsize control reducing the current stepsize whenever Eq. (9) has no finite solution seems natural. An improved simulation procedure with flexible stepsize control is presented in Algorithm 3, where in each step of simulation, the procedure first tries to find a finite upper bound e satisfying Eq. (9) with an initial stepsize $\tau _0$. If it fails, the current interval is split into two (line 15) and the above operations repeat. Termination of refining the stepsize is guaranteed by the continuous differentiability of $\varvec{f}$ in both of its arguments. Along with variation of $\tau$, the bias locating the delayed state within the list of sampling points need to be recomputed in each step by a backward search (line 8). This may generate extra error, as the nearest sampling point $\mathbf {y}_{n-m}$ may not feature exactly the desired delay. This additional error is accounted for by modifying the first line of the constrained optimization (9) into

$$\begin{aligned} \Vert (\mathbf {x}+ t_1*\mathbf {f}, \mathbf {u}+ t_2*\mathbf {g}) - \varvec{f}(\mathbf {y}_n,\mathbf {y}_{n-m}) \Vert \le e-\sigma \end{aligned}$$

(10)

for any $t_1, t_2\in [0,\tau ]$. The correctness and completeness arguments for Algorithm 3 are akin to Theorem 2.

5 Implementation and Experimental Results

To evaluate the approach of verification along simulations, we have implemented the proposed algorithms with local stepsize control as a prototype⁴ in Matlab. It takes a time-bounded safety verification problem of delayed dynamical systems as input, and it terminates with one of the three results SAFE, UNSAFE, or UNKNOWN, reflecting the fact that a fine enough over-approximation has been found to prove the system safe or unsafe, respectively, or that the maximum permitted density of covering the initial set was insufficient for obtaining a definite answer.

As our algorithm relies on solving the constrained optimization problems (9) or (10), resp., for determining validated bounds, we have tried different solvers for discharging that optimization problem, namely the numerical (and thus devoid of formal guarantees concerning completeness and soundness) procedure fmincon provided by Matlab and the optimization-modulo-theory procedure offered by the nonlinear SAT-modulo theory solver HySAT II ⁵ [16]. The constrained optimization problems (9) and (10) involve a universally quantified constraint of the shape

$$\begin{aligned} \text {find } \min \{e \ge 0 \mid \forall x: \phi (x,e) \implies \psi (x,e)\}, \end{aligned}$$

(11)

which is outside the scope of the above solving procedures, as these handle existential constraints only. We therefore have substituted (11) by the existentially constrained optimization problem

$$\begin{aligned} \text {find } \max \{e \ge 0 \mid \exists x: \phi (x,e) \wedge \lnot \psi (x,e)\}. \end{aligned}$$

(12)

Due to the linear ordering on $\mathbb {R}_{\ge 0}$, problem (12) is guaranteed to yield an upper bound on the solution of (11), which is safe in our context. Both fmincon and HySAT II proved to be able to efficiently solve (9) and (10) in the formulation (12), with HySAT II being able to provide a validated solution due to global search based on a combination of interval constraint propagation with optimization-modulo-theory solving.

HySAT II [16] is a sat-modulo-theory (SMT) solver accepting formulas containing arbitrary boolean combinations of theory atoms involving linear, polynomial and transcendental functions. It internally rewrites these formulae into an equi-satisfiable conjunctive normal form by means of a definitional translation introducing auxiliary propositional and numeric variables representing the truth values of sub-formulae and the numeric values of subexpressions, resp., thus generalizing the well-known Tseitin transformation [25]. HySAT II then solves the resulting CNF through a tight integration of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm [6] in its conflict-driven clause learning (CDCL) variant with interval constraint propagation (ICP) [3]. Details of the algorithm, which operates on interval valuations for both the Boolean and the numeric variables and alternates between choice steps splitting such intervals and deduction steps narrowing them based on logical deductions computed through ICP or Boolean constraint propagation (BCP), can be found in [14]. Implementing a branch-and-prune search in interval lattices and conflict-driven learning of clauses comprising irreducible atoms in those lattices, it can be classified as an early implementation of abstract conflict-driven clause learning (ACDCL) [4].

By this ACDCL proof search, HySAT II will successively construct a cover of the actual solution set of the constraint problem by tiny interval boxes, a sequence of so-called candidate solution boxes together enclosing all solutions. Optimization then is based on a branch-and-prune search over the candidate solution boxes, which is straightforward to integrate into the ACDCL proof search by biasing the ACDCL splitting rule to better values when splitting along the variable representing the optimization criterion, plus learning bounds that impose blocking on any solutions worse than the best value up-to-now found.

The soundness of this procedure for solving the optimization problems (9) or (10) in the formulation (12) follows immediately from the soundness properties of ICP, which narrows the search space by chopping off regions not containing any solution, but will never remove solutions [3]. It consequently is an invariant of the iSAT algorithm’s proof search, as implemented in HySAT II, that its residual search space internally represented by interval boxes plus the already reported solution boxes together safely over-approximate the actual solution space [14]. This in turn implies that the maximum found by HySAT II always is a safe upper bound of the actual maximum, irrespective of possible non-convexity of the optimization problem at hand. We can conclude that solving the optimization problems (9) or (10) in the formulation (12) with HySAT II will provide a safe upper bound on the actual optimal value of (12), which in turn is an upper bound on (9) or (10), resp., in the original form (11). As any upper bound renders the enclosure in Algorithms 2 or 3, resp., correct, we can conclude that HySAT II’s optimization procedure guarantees soundness of the overall algorithm. The possible failure of HySAT II’s optimization procedure in determining a sharp over-approximation of the optimal value will at most impact performance, as it may enforce an unnecessarily dense cover by simulation traces due to overly pessimistic bloating of the original traces.

In the following, we demonstrate our approach by verification of some quintessential DDEs.

Delayed Logistic Equation. In 1948, G. Hutchinson [17] introduced the delayed logistic equation

$$\begin{aligned} \dot{n}(t) = a [1-n(t-T)/K] n(t) \end{aligned}$$

to model a single population whose percapita rate of growth at time t

$$\begin{aligned} \dot{n}(t)/n(t) = a [1-n(t-T)/K] \end{aligned}$$

depends on the population size T times 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 those to recover its availability. If we let $N(t)=n(t)/K$ and rescale time, then we get the discrete-delay logistic equation

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

(13)

Arguments in [24] established that for any initial function $N_0>0$, there exists a unique non-negative solution $N(\phi ,t)$ defined for all $t>0$. Wright’s conjecture [26], still unsolved, is that if $r \le \pi /2$ then $N(\phi ,t) \rightarrow 1$ as $t \rightarrow \infty$ for all solutions of Eq. (13) satisfying $N_0>0$.

Fig. 1.

Over-approximation of the solutions of Eq. (13) originating from region $\mathcal {B}_{0.01}(1.49)$ under delay $r = 1.3$. Initial stepsize $\tau _0 = 0.01$, time bound $T = 10$ s.

Fig. 2.

Over-approximation rigorously proving Eq. (13) unsafe, with $r = 1.7$, $\mathcal {X}_0 = \mathcal {B}_{0.025}(0.425)$, $\tau _0 = 0.1$, $T = 5$ s and $\mathcal {U}= \{ N|N>1.6 \}$.

Fig. 3.

The logistic system (13) is proven safe through 6 rounds of simulation with base stepsize $\tau _0 = 0.1$. Delay $r = 1.3$, initial state set $\mathcal {X}_0 = \{N | N \in [0.5,1.5]\}$, time bound $T = 5$ s, unsafe set $\{N|N>1.6\}$.

Figure 1 illustrates an over-approximation of trajectories of Eq. (13) in terms of a specific initial set. It provides an intuitive description of our simulation approach equipped with computation of on-the-fly linear local error bounds. To investigate Wright’s conjecture, we further explore the safety verification framework based upon validated simulations with a delay $r=1.3 < \pi /2$, for which the trajectories are expected to converge within a time interval. The detailed verification process is elaborated in Fig. 3. Meanwhile, we also successfully falsified an unsafe case with $r=1.7$ where the over-approximation of a diverging trajectory can be rigorously shown to violate the safety property (see Fig. 2).

Delayed Microbial Growth. Ellermeyer et al. [10, 11] introduced a delay in the standard bacterial growth model in a chemostat which, after scaling time and the dependent variables, can be written as

$$\begin{aligned} \begin{array}{@{}lcl} \dot{S}(t) &{}=&{} 1-S(t)-f(S(t))x(t)\, ,\\ \dot{x}(t) &{}=&{} \mathrm {e}^{-r}f(S(t-r))x(t-r)-x(t)\, ,\\ \end{array} \end{aligned}$$

(14)

where $f(S) = \alpha S/(\beta +S)$, and S(t) denotes the substrate (food for bacteria) concentration, while x(t) is the biomass concentration of bacteria. The delay r reflects the assumption that whereas cellular absorption of substrate is assumed to be an instantaneous process, a resulting increase in microbial biomass reflecting assimilation is assumed to lag by a fixed amount of time r. A specific verification problem of Eq. (14) is shown in Fig. 4, where different rounds of simulation are depicted together in the phase space of S and x, and for a clear presentation, we only sketch the over-approximations around those numerically computed sampling points.

Fig. 4.

Equation (14) is proven safe by 17 rounds of simulation w. $\tau _0 = 0.45$. The simulated trajectories start from within a cover of $\mathcal {X}_0$ (the red dashed circle on the right) and converge eventually to a basin of attraction (marked by a small blue rectangle). Here, $\alpha = 2\mathrm {e}$, $\beta = 1$, $r = 0.9$, $\mathcal {X}_0 = \mathcal {B}_{0.3}((1;0.5))$, $\mathcal {U}= \{(S;x)|S+x<0\}$, $T = 8$ s.

Gene Regulation. To further investigate the scalability of our approach to high dimensions, we recall an instantiation of Example 1 by setting $n=5$, namely with 5 state components $\mathbf {x}= (x_1;x_2;\ldots ;x_5)$ and 5 delay terms $\mathbf {r}= (r_1;r_2;\ldots ;r_5)$ involved. This essentially yields, in each step of simulation, an optimization procedure of the form (10) with 23 scalar variables, i.e., $e,t_1,t_2$ and $\mathbf {x},\mathbf {u},\mathbf {f},\mathbf {g} \in \mathbb {R}^5$. By further setting $\mathbf {r}= (0.1;0.2;0.4;0.8;1.6)$, $\mathcal {X}_0 = \mathcal {B}_{0.2}((1;1;1;1;1))$, $\mathcal {U}= \{{\mathbf {x}|x_1<0}\}$, and $T = 2$ s, the system of Eq. (4) is rigorously proven unsafe, which means that the dosage of mRNA might degrade to negative in this hypothetical setting.

As an intuitive observation, the verification time consumed by our prototype is fairly sensitive to the specific setting of the verification problem, including the initial set $\mathcal {X}_0$, the delays $\mathbf {r}$, the unsafe set $\mathcal {U}$, and the time bound T as well. However, the optimization routine proved well scalable to high dimensions, and particularly, verifications of the above benchmark systems all completed successfully in a handful of minutes.

6 Conclusion and Future Work

We have exposed an approach for automated formal verification of time-bounded reachability properties of a class of systems that feature delayed differential dynamics governed by delay differential equations (DDEs) with multiple different delays (including 0, i.e., direct feedback). This class of system models has successfully been used to model various real-world systems in the field of biology, control theory, economics, and other domains. Our approach is based on adapting the paradigm of verification-by-simulation to DDEs. It provides bounded-time verification by covering the full set of time-bounded trajectories of a dynamical system evolving from the initial state set by means of investigating a finite sample of initial states plus generalization via a sensitivity argument. Initially, it triggers a finite set of numerically approximate simulations of the dynamic behaviors, thereby generating a finite set of approximate simulation traces originating from a finite sample of the initial states. As the sample does not cover all initial states, and as simulation is only approximate, we bloat each time-stamp value pair returned from the simulation by a distance determined via an error bound computed automatically on-the-fly during simulation. This error bound incorporates both sensitivity information concerning start states and rigorous bounds on integration error incurred by numerical solving. Hence, the union of the state sets reached by all the individual bloated trajectories provides a safe over-approximation of the states actually reachable from the initial set within the time bound. If this over-approximation proves safety in the sense that the reachable states do not intersect the unsafe states, or conversely if the simulation produces a valid counter-example in the sense that it can prove that a trajectory hits the unsafe states, then the algorithm generates the corresponding verdict. Otherwise, our algorithm refines its sample of initial states and repeats the previous steps to compute a more precise over-approximation.

Based on that approach, we have implemented a prototype of a validated solver for DDE. Using it, we have successfully demonstrated the method on several benchmark systems involving delayed differential dynamics.

As a future work, we plan to replace Euler’s direct method by high-order Runge-Kutta methods [1] in order to obtain more precise approximations. Furthermore, the method of Zou et al. [27] can be extended to provide a safe enclosure algorithm for the class of systems (3) suitable for use in unbounded formal verification, based on the fact that the iSAT constraint solver [14] used therein supports unbounded verification by means of Craig interpolation. In addition, it could be quite interesting to investigate how to combine the technique of conformance testing for hybrid systems [18, 23] with our approach. The potential merits of such combination is twofold: on the one hand, it can extend the conformance testing technique to deal with hybrid systems with delays; on the other hand, it may improve the efficiency of the conformance testing technique by using simulation-based approach to over-approximate the reachable set instead of directly computing.