Keywords

1 Introduction

All scientific branches share the common concept of modeling. When a scientist studies a real-life system, the first step he or she goes through is to build a model that gathers all the existing knowledge of the target system. This model is then used as a proxy of the system it represents in order to analyze it, perform simulation or predictions. In several fields, such as Biology, Chemistry, Physics or Engineering, models do not represent a single system but are instead an abstraction for a family of systems that share common traits but might exhibit some internal variability. This internal variability can either be left out by considering that the model represents the “average” individual in the family, or taken into account inside of the model through the use of non-determinism, probabilities or parametricity.

When considering parametric models, scientists have to go through a phase of parameterization, which consists in confronting the model with experimental observations of the (family of) system(s) it represents in order to find the parameter values that best fit this (family of) system(s). In most cases, parameterization techniques are deterministic [21, 24]. They lead to deterministic parameter values that best fit the experimental data, i.e. producing the best fit for the “average” individual. In this paper, we instead focus on a technique that allows to select parameter values that best fit under variability, i.e. that produce the best probabilistic fit for the whole family.

Parameterization, or parameter synthesis has been the topic of many works in the context of probabilistic systems [6, 9,10,11, 13]. Symbolic techniques such as parametric model checking [1, 5] are often difficult to use in practice because they require automata-based models while real-life models are often expressed either with computer programs or with differential equation models. Statistical Model Checking (SMC) [14], on the other hand, is a simulation-based technique that allows to estimate, with formal guarantees, the probability that a given (probabilistic) model satisfies a given property. Because it is simulation-based, it can be applied to any stochastic model for which simulations can be performed. SMC has been successfully applied to perform parameterization of real-life models expressed using several formalisms such as parametric Markov chains [2], parametric Python programs [20], or even parametric Ordinary Differential Equation systems (ODEs) [15]. Unfortunately, the formal guarantees obtained through SMC are linked to the simulation space (i.e. the produced traces) and not to the original model itself. When the model consists in sets of ODEs, as in [15], numerical resolution methods are used in order to solve the ODEs and perform simulations, which means that the formal guarantees obtained through SMC cannot apply to the original ODE model.

In this paper, our main contribution is to bridge the gap between the original ODE model and the results of the parameterization procedure by combining the statistical guarantees of SMC with the global approximation error of standard numerical resolution methods. As in [15], we consider ODE models with structural parameters. We assume that these models represent families of real-life systems that need to match some experimental data through simulation. We build on the logic proposed in [15] to express our properties of interest and also consider expected reward properties that might be of interest in practice. We use SMC to grade parameter values by estimating the expectation of a given reward function for these values while taking internal variability into account. Contrarily to what is done in [15], the accuracy of this estimation is guaranteed w.r.t. the original ODE model.

To illustrate our results, we perform the parameterization of two state-of-the-art models taken from the literature using our technique. In this context, and because modelers are often interested by this information in practice, we propose a global evaluation of the parameter space that allows us to get a complete picture of the adequacy of the parameter values w.r.t. the given experimental data. This choice is done by interest only, since our results are generic and could be applied to any search technique, such as the local ones performed in [15].

Intuition. To give an intuition of our contribution, we provide an informal summary of the method we present in this paper. Recall that, given a dataset relative to an experiment and a parametric ODE system, the objective is to find a solution to a parametric ODE system (i.e. parameter values) that satisfies a property \(\varphi \) w.r.t. the dataset, which is, given a distance \(\delta > 0\), “the solution stays in a tunnel of radius \(\delta \) around the experimental data”; we also want to acquire statistical guarantees on said result. The main issue is that we can only simulate our model by solving the ODE system using numerical resolution methods. Hence, we cannot directly verify whether exact solutions (z) of the system satisfy \(\varphi \) and instead have to rely on approximate solutions (y). We therefore proceed as follows: we start by discretizing the set of parameter values into a grid; we then evaluate each point of this grid using the procedure detailed below; finally, we use the resulting scores to select the “best” parameter values w.r.t \(\varphi \). The score of a given parameter value \({\boldsymbol{\lambda }}\) is computed as follows, and illustrated in Figs. 1 and 2 in the context of the case study presented in Sect. 4.1.

  1. 1.

    We set the parameter value to \({\boldsymbol{\lambda }}\). By a careful study of the ODE system, we give a bound on the distance \(\varepsilon \) between exact (z) and approximate (y) solutions. We emphasize that this bound depends on (1) the chosen resolution technique and (2) the chosen integration step. We show that this distance is uniformly stable w.r.t. internal variability around \({\boldsymbol{\lambda }}\), but also that it can be uniformly bounded on the global set of solutions (i.e. independently of \({\boldsymbol{\lambda }}\)).

  2. 2.

    We propose two new properties \(\varphi _1\) and \(\varphi _2\) that will be verified on the approximate solutions y, and depend on the above distance. This amounts to changing the size of the tunnel around the experimental dataset. We compute (estimations of) the respective probabilities \(p_1\) and \(p_2\) and prove that the probability p that z satisfies \(\varphi \) lies between \(p_1\) and \(p_2\).

  3. 3.

    We provide statistical guarantees of our estimation, i.e. a confidence interval for our estimation of p, and use this estimation as the score for parameter value \({\boldsymbol{\lambda }}\).

Fig. 1.
figure 1

Tunnels corresponding to the properties \(\varphi ,\varphi _1,\varphi _2\) and accepted simulations.

Full size image
Fig. 2.
figure 2

\(\varphi \)-accepted, \(\varphi _2\)-accepted and rejected solutions.

Full size image

It is worth noting that the underlying theory is generic: the integration method as well as the statistical estimation method can be chosen arbitrarily as long as they provide the usual guarantees. In this paper, we use Runge-Kutta and Monte-Carlo for the sake of example.

Outline. In Sect. 2, we introduce required preliminaries and notations for the rest of the paper. In Sect. 3, we state the main result of the paper, i.e. we compute the approximation error for ODE solutions, show that this error is uniformly stable, and provide the statistical guarantees for the estimation of the probabilities. In Sect. 4, we illustrate our approach on two case studies taken from the literature. Finally, we conclude in Sect. 5 and give perspectives for future work.

2 Background and Notations

In this section, we present the basic notations and definitions that will be used throughout the paper. More precisely, we recall the definition of an ODE, and present the logic used in the paper. Finally, we extend this logic by introducing reward functions.

2.1 ODE Preliminaries

First, we consider an evolution problem described by an Ordinary Differential Equation (ODE) of the form

$$\begin{aligned} \frac{\textrm{d}z}{\textrm{d}t}(t) = f\big (z(t), {\boldsymbol{\lambda }}\big ), \quad t > 0. \end{aligned}$$
(1)

In Eq. (1), the unknown function z is defined in \(\mathbb {R}^+\) with values in \(\mathbb {R}^n\); \({\boldsymbol{\lambda }}\in \mathbb {R}^m\) is a vector of parameters; f is a function defined on \(\mathbb {R}^n \times \mathbb {R}^m\) with values in \(\mathbb {R}^n\), whose regularity will be detailed below; n, m are positive integers. In the following, we write \(z_i(t)\), \(1\le i \le n\), for the projection of z(t) on its ith component. As mentioned in our introduction, Eq. (1) can model various real-world problems arising in life sciences. Our goal is to study some properties of the trajectories determined by Eq. (1), by developing an innovative model-checking framework suitable for the continuous dynamics of ODEs.

Here and for the rest of the paper, we fix an initial condition \(z_0 \in \mathbb {R}^n\). Standard results of the theory of differential equations (see for instance [18]) ensure that, for any value of the parameter \({\boldsymbol{\lambda }}\in \mathbb {R}^m\), the Cauchy problem determined by Eq. (1) and the initial value \(z(0) = z_0\) admits a unique solution, provided f is \(C^1\) on \(\mathbb {R}^n \times \mathbb {R}^m\); we denote by \(z^{\boldsymbol{\lambda }}(t)\) the corresponding trajectory, which we assume to be defined on [0, T] with \(T > 0\). If the context is sufficiently clear, we may write z(t) for short. As before, we write \(z_i^{\boldsymbol{\lambda }}(t)\) (resp. \(z_i(t)\)), \(1 \le i \le n\), for the projection on its ith component. We assume that the component \(\lambda _j\) of the parameter vector \({\boldsymbol{\lambda }}\in \mathbb {R}^m\) (\(1 \le j \le m\)) satisfies \(\lambda _j \in [L_j^{\boldsymbol{\lambda }}, U_j^{\boldsymbol{\lambda }}]\), with real coefficients \(L_j^{\boldsymbol{\lambda }}< U_j^{\boldsymbol{\lambda }}\) and we consider the compact sets \(\textbf{W}\) and \(\textsf{INIT}\) defined by

figure a

For \({\boldsymbol{\lambda }}\in W\), we consider the Euclidean norm defined by \(\left\| {\boldsymbol{\lambda }}\right\| = \left( \sum _{j=1}^m \left| \lambda _j\right| ^2\right) ^{1/2}\).

We assume that the trajectories of Eq. (1) starting from \(z_0\) admit a rectangular invariant region, uniform w.r.t. the parameter \({\boldsymbol{\lambda }}\), that is \(z_i(t, {\boldsymbol{\lambda }}) \in [L_i, U_i]\) for \(t \in [0, T]\), with real coefficients \(L_i < U_i\), for all \({\boldsymbol{\lambda }}\in \textbf{W}\) and for \(1 \le i \le n\). The global invariant region for z is written \(\textbf{V}= \prod _{i = 0}^n [L_i, U_i]\).

Finally, we write \(\textsf{TRAJ}\) for the set of all potential trajectories of the solutions to our ODE system. Formally, \(\textsf{TRAJ}= \{z^{\boldsymbol{\lambda }}(t) ~|~ {\boldsymbol{\lambda }}\in \textbf{W}\}\).

It is well-known that Eq. (1) determines time continuous trajectories, which moreover depend continuously on a variation of the initial condition \(z_0\) and of the parameter \({\boldsymbol{\lambda }}\in \textbf{W}\) (see for instance [18]). In Sect. 3, we will be interested in the variation of those trajectories under a variation of the parameter \({\boldsymbol{\lambda }}\in \textbf{W}\). We now move to the description of the properties for our models.

2.2 Bounded Linear Time Logic

As explained in the introduction, our aim is to find the parameter values that allow our model to best fit some given experimental data. In the following, we therefore assume that we are given a finite set of experimental observations that correspond to a finite set of time points and a tolerance value \(\delta >0\)Footnote 1. We write

$$\begin{aligned} \mathcal {T}= \{0 = t_0, t_1, \dots , t_N = T\} \end{aligned}$$
(4)

for a set of time points and assume that we have a finite set of observations \(\mathcal {O}_i^t = \{o_{i,1}^t, \ldots , o_{i,k}^t\}\) for each of them and for each coordinate i. We assume, in practice, that \(\mathcal {T}\) indeed includes all the time points where experimental observations are available. Remark nonetheless that \(\mathcal {T}\) is not necessarily limited to this set, as we could have \(\mathcal {O}^t = \emptyset \) for a number of \(t \in \mathcal {T}\). In practice, since \(\mathcal {T}= \{t_0, \ldots t_N\}\) is finite, we abuse notations and substitute it, when convenient, with the integer set \(\mathcal {T}= \{0, \ldots N\}\).

We start by recalling the logic defined in [15], which allows to express our properties of interest, i.e. that a given solution agrees with the experimental observations available at given time points. This logic is a slightly modified version of Bounded LTL, where atomic propositions are of the form (i, l, u) with \(L_i \le l \le u \le U_i\), where \(L_i\) and \(U_i\) are the boundaries of the set \(\textbf{V}\) defined above. The intuition is that, for \(q \in \mathcal {T}\), z satisfies the atomic proposition (i, l, u) at time point q if and only if \(l \le z_i(q) \le u\). Since there is a finite number of time points and a finite number of observations, we only consider the finite number of atomic propositions where \(1 \le i \le n\) and \(l,u \in \cup _{q \in \mathcal {T}} (\mathcal {O}_i^q\cup \mathcal {O}_i^q-\delta \cup \mathcal {O}_i^q+\delta )\). We also allow \(l,u = +\infty , -\infty \) to account for timepoints q where \(\mathcal {O}^q = \emptyset \).

The rest of the logic is defined as usual:

  • every atomic proposition and the constants true, false are BLTL formulas,

  • the negation and conjunction of BLTL formulas are BLTL formulas,

  • if \(\varPsi \) and \(\varPsi '\) are BLTL formulas, then \(\varPsi \mathcal {U}^q \varPsi '\) and \(\varPsi \mathcal {U}^{\le q} \varPsi '\) are BLTL formulas for any positive integer \(q \in \mathcal {T}\),

  • if \(\varPsi \) is a BLTL formula, then \(\mathcal {X}\varPsi \) is a BLTL formula.

The interpretation of \(\varPsi \mathcal {U}^{\le q} \varPsi '\) is standard, i.e. \(\varPsi '\) must happen before q time points have elapsed, while the interpretation of \(\varPsi \mathcal {U}^q \varPsi '\) is that \(\varPsi \) must hold for exactly q time points before \(\varPsi '\) holds. The interpretation of \(\mathcal {X}\varPsi \) is standard as well, i.e. \(\mathcal {X}\varPsi \Leftrightarrow true \mathcal {U}^1 \varPsi \). We invite the interested reader to consult [15] for the formal semantics of this logic.

Given a BLTL formula \(\varPsi \), we define \(\textsf{models}(\varPsi ) = \{z \in \textsf{TRAJ}~|~ z,0 \models \varPsi \}\).

Recall that the properties we want our models to verify are the following: the traces of the model need to agree with the given experimental data. One way to rephrase this property is as follows: at all time points where experimental data is available, the trace of our model needs to be between the lower and upper values taken from the experimental data with a given tolerance \(\delta >0\). This is easily expressed in BLTL as the property

$$\begin{aligned} \varPsi ^* = \bigwedge _{1 \le i \le m}\psi _i^0 \wedge \mathcal {X}\left( \psi _i^1 \wedge \mathcal {X}(\psi _i^2 \wedge \dots \wedge \mathcal {X}\psi _i^N)\dots \right) \end{aligned}$$
(5)

where \(\psi _i^q = (i, \min (\mathcal {O}_i^q) - \delta , \max (\mathcal {O}_i^q) + \delta )\). Since our aim is to consider variability on the ODE models of interest, we may use statements of the form \(\mathbb {P}_{\ge p}(\varPsi ^*)\), whose interpretation is expressed as follows: “the probability that a trajectory in \(\textsf{TRAJ}\) is in \(\textsf{models}(\varPsi ^*)\) is greater than p”. In this regard, we need to define a probability measure \(\mathbb {P}\) over \(\textsf{TRAJ}\).

We start by noticing that each parameter value \({\boldsymbol{\lambda }}\) completely determines the trajectory \(z^{\boldsymbol{\lambda }}\in \textsf{TRAJ}\), since the initial condition \(z_0 \in \mathbb {R}^n\) has been fixed. As a consequence, \(\textsf{TRAJ}\) can be completely identified with \(\textsf{INIT}\) (see Eq. (3)). Formally, we define \(\textsf{Models}(\varPsi ) \subseteq \textsf{INIT}\) as the set

$$\begin{aligned} \{(z_0,{\boldsymbol{\lambda }}) \in \textsf{INIT}~|~ z^{\boldsymbol{\lambda }}(t) \in \textsf{models}(\varPsi )\} \end{aligned}$$
(6)

and consider the \(\varSigma \)-algebra \(\mathscr {B}\) generated by the m-dimensional open intervals of \(\textsf{INIT}\). As expected, it is shown in [15] that \(\mathscr {B}\) is an adequate support to prove the measurability of \(\textsf{Models}(\varPsi )\) for any BLTL formula \(\varPsi \).

In the following, we will consider a number of probability distributions \(\mathbb {P}^{\boldsymbol{\lambda }}\) on \(\mathscr {B}\) (one for each parameter value \({\boldsymbol{\lambda }}\)), and use these probability distributions to evaluate whether our ODE model meets a specification of the form \(\mathbb {P}^{\boldsymbol{\lambda }}_{\ge p}(\varPsi )\). This will amount to checking whether \(\mathbb {P}^{\boldsymbol{\lambda }}(\textsf{Models}(\varPsi )) \ge p\). We will refer to the formulas such as \(\mathbb {P}^{\boldsymbol{\lambda }}_{\ge p}(\varPsi )\) as PBLTL formulas.

In our context, each parameter value \({\boldsymbol{\lambda }}\) in \(\textbf{W}\) will give rise to a probability distribution \(\mathbb {P}^{\boldsymbol{\lambda }}\) taking into account internal variability. This probability distribution will be used for evaluating the model against the property \(\varPsi ^*\), which will yield a score \(\textsf{grade}({\boldsymbol{\lambda }})\) that represents the adequacy of parameter value \({\boldsymbol{\lambda }}\) w.r.t. the given experimental data while taking into account internal variability.

However, it might happen that many of the values \({\boldsymbol{\lambda }}\) in \(\textsf{INIT}\) have a maximal score \(\textsf{grade}({\boldsymbol{\lambda }}) = 1\), i.e. satisfy the PBLTL property \(\mathbb {P}^{\boldsymbol{\lambda }}_{\ge 1}(\varPsi ^*)\). This could be the case for example if all the traces generated using \(\mathbb {P}^{\boldsymbol{\lambda }}\) satisfy the property \(\varPsi ^*\). In this case, we will need to consider more complex properties to filter those values and rank them. To this purpose, we introduce the notion of reward function.

2.3 Reward Function

The purpose of statistical model checking in general, and Monte-Carlo in particular, which will be presented in detail in Sect. 3.2, is to estimate with formal guarantees the expected value of a given function on a measurable set. In the context of model checking, this procedure is used to estimate the probability that a given model satisfies a property. To do this, each sample of the system is checked against the property and a Boolean reward is computed accordingly (i.e. 1 if the property is satisfied and 0 otherwise). Statistical model checking then amounts to estimating the expected value of this particular reward function on the measurable set of traces of the model at hand.

In our case, this boils down to defining a reward function \(r_{\varPsi ^*} : \textsf{TRAJ}\rightarrow \lbrace 0,1 \rbrace \) that evaluates to 1 if the trajectory satisfies \(\varPsi ^*\) and 0 otherwise. Statistical model checking will then compute an estimation of the expected value of \(r_{\varPsi ^*}\) on the set of traces \(\textsf{TRAJ}\) under the probability distribution \(\mathbb {P}^{\boldsymbol{\lambda }}\), which in the end will be an estimation of the measure of \(\textsf{Models}(\varPsi ^{*})\) for the parameter value \({\boldsymbol{\lambda }}\). Remark that this construction would work for any other BLTL property \(\varPsi \).

In order to grade the parameter values in a more discriminating way, we allow the use of non-Boolean reward functions. This will allow expressing more powerful properties than those that can be defined using the BLTL logic. For instance, one can use those reward functions in order to measure the number of time points for which the current trace does not agree with the given experimental data, or to measure the cumulative distance between the trace and the experimental data at all time points.

In the following, we will therefore consider a given reward function \(r : \textsf{TRAJ}\rightarrow \mathbb {R}\) and use statistical model checking to estimate its expected value on the trajectories of our model under a given probability distribution \(\mathbb {P}\). When convenient, we will identify a given BLTL property \(\varPsi \) with its associated reward function obtained through the above construction \(r_\varPsi \).

3 Global Statistical Guarantees

In this section, we state our main result, which provides statistical guarantees on the verification of specific properties. Namely, given a property \(\varPsi \) (resp. the corresponding reward function \(r_\varPsi \)) on the trajectories of Eq. (1), we will establish confidence intervals regarding the estimation of the probability of satisfaction of that property (resp. the expected value of \(r_\varPsi \)), which shall be computed using approximate solutions to Eq. (1), as well as a bound on the errors w.r.t. the exact probability corresponding to the exact solutions to Eq. (1).

We start by recalling how ODE numerical resolution methods work, and we propose a definition for the approximation errors introduced in the process. Next, we introduce a method for estimating the probability p that exact solutions of our ODE system satisfy a given property \(\varPsi \) using an estimator \(\hat{p}\) that takes the approximation error into account. Finally, we explain how those results along with their statistical guarantees can be extended to the estimation of the expected values of given reward functions.

3.1 Approximation Method for the Numerical Integration of the ODE

We recall that an approximation method, which determines the approximate solution \(y^{\boldsymbol{\lambda }}\) to the ODE induced by parameter \({\boldsymbol{\lambda }}\), can be written

$$\begin{aligned} y^{\boldsymbol{\lambda }}(0) = z_0, \quad y^{\boldsymbol{\lambda }}(\tau _{j+1}) = y^{\boldsymbol{\lambda }}(\tau _j) + h \, \varPhi \big (\tau _j, y^{\boldsymbol{\lambda }}(\tau _j), {\boldsymbol{\lambda }}, h \big ), \quad 0 \le j < J, \end{aligned}$$
(7)

where \(\varPhi \) is a continuous function defined in \([0,T] \times \mathbb {R}^n \times \textbf{W}\times \mathbb {R}\) with values in \(\mathbb {R}^n\), \(\tau _j\) are the discrete points of definition of \(y^{\boldsymbol{\lambda }}\), and \(h \in \mathbb {R}\). Intuitively, those methods compute each point thanks to the previous one. In this paper, we use the well-known Runge-Kutta 4 method, which is a standard method for ODE resolution.

For the sake of simplicity, we focus in the following on the theoretical study of 1-dimensional systems (\(n = 1\)), but our method can be adapted to larger systems (\(n \ge 2\)) as shown in our second case study presented in Sect. 4.2, mostly by adapting the definition of distance introduced below.

As explained in Sect. 2, we consider a set \(\gamma \) of observation data samples, recorded at \((N+1)\) time points forming a set \(\mathcal {T}\) (see Eq. (4)) with values in \(\mathbb {R}^n\) (\(N>0\)). We start by defining a notion of distance between functions that will, in the end, allow us to compare the solutions of our ODE model with the given experimental data. Given any two functions \(y, \tilde{y}\) in the set \(F_\mathcal {T}= \{g\,: I \rightarrow \mathbb {R}\,|\, \mathcal {T}\subseteq I\}\), where I denotes an interval included in \(\mathbb {R}\), we consider the distance d defined by

$$\begin{aligned} d(y, \tilde{y}) = \max _{t \in \mathcal {T}} \left| y(t) - \tilde{y}(t)\right| . \end{aligned}$$
(8)

Note that d is rigorously only a pseudo-distance, since two functions y and \(\tilde{y}\) defined on [0, T], that are distinct on [0, T], might coincide on the finite set \(\mathcal {T}\), thus could satisfy \(d(y, \tilde{y}) = 0\). Nevertheless, since our purpose is to measure the distance to the dataset \(\gamma \), we do not need to distinguish such two functions. Moreover, one may use any (pseudo-)distance of their choice, since all norms are equivalent in the finite-dimensional space \(\mathbb {R}\) (\(\mathbb {R}^n\) in the general setting). In the rest of the paper, we will abuse notations and use d to compare a given function \(y \in F_\mathcal {T}\) to \(\gamma \), even though \(\gamma \) is only defined on \(\mathcal {T}\) and not on a continuous subinterval of \(\mathbb {R}\).

In most ODE resolution methods, the approximation error depends on an integration step. We therefore introduce a discretization \(\mathcal {D}_h\) of the time interval [0, T], which we assume, for simplicity, to admit a constant step \(h>0\):

$$\begin{aligned} \mathcal {D}_h = \lbrace 0 = \tau _0, \tau _1, \tau _2, \dots , \tau _J = T \rbrace , \end{aligned}$$
(9)

with \(J >0\) and \(\tau _{j+1} - \tau _j =h\) for all \(0 \le j < J\).

For each parameter value \({\boldsymbol{\lambda }}\in \textbf{W}\), the chosen approximation method will compute an approximate solution to the ODE, which we denote \(y^{\boldsymbol{\lambda }}\). Recall that the initial condition \(z_0 \in \mathbb {R}\) (\(\mathbb {R}^n\) in the general setting) has been fixed and that for any \({\boldsymbol{\lambda }}\in \textbf{W}\), the exact solution to Eq. (1) such that \(z(0) = z_0\) is written \(z^{\boldsymbol{\lambda }}\).

For the sake of measuring the approximation error between \(y^{\boldsymbol{\lambda }}\) and \(z^{\boldsymbol{\lambda }}\), we use a finer notion of distance than the one proposed above. Indeed, standard resolution methods provide guarantees that depend on the integration step in the sense that choosing a finer integration step enhances the quality of the approximation. Our aim here is to be able to take advantage of this fact, which could not be captured if we used the distance d from Eq. (8).

Definition 1 (Global approximation error)

Let \(h>0\) be the integration step of the chosen resolution method. The global approximation error \(\epsilon _h({{\boldsymbol{\lambda }}})\) between the approximate solution \(y^{\boldsymbol{\lambda }}\) and the exact solution \(z^{\boldsymbol{\lambda }}\) is defined as follows:

$$\begin{aligned} \epsilon _h({{\boldsymbol{\lambda }}}) = \max _{\tau \in \mathcal {D}_h} \left| z^{\boldsymbol{\lambda }}(\tau ) - y^{\boldsymbol{\lambda }}(\tau )\right| . \end{aligned}$$
(10)

In the rest of the paper, we make two important assumptions on the approximation method. First, we assume that the set \(\mathcal {T}\) of time points given by Eq. (4), at which the observation data \(\gamma \) are recorded, satisfies \(\mathcal {T}\subset \mathcal {D}_h\). This assumption is quite natural as there are a finite number of experimental data, therefore a sufficiently small h can always be chosen accordingly. Our second assumption is that the approximation method is convergent, which guarantees that for all \({\boldsymbol{\lambda }}\in \textbf{W}\), the global approximation error \(\epsilon _h({{\boldsymbol{\lambda }}})\) converges to 0 when h gets smaller. This latter assumption is directly satisfied for usual approximation methods (such as, e.g., Runge-Kutta; see for instance [3]).

3.2 Monte-Carlo Method

We now move to our main result, i.e. providing an estimation of the probability that the original ODE system, with a given parameter value \({\boldsymbol{\lambda }}^*\), agrees with the experimental data with statistical guarantees. For the sake of simplicity, we focus in this section on standard BLTL properties as introduced in Sect. 2.2. We then show in Sect. 3.3 how these results can be extended to reward functions.

Let \({\boldsymbol{\lambda }}^* \in \textbf{W}\) be a parameter value. In order to take the internal variability of our system into account, we will consider that \({\boldsymbol{\lambda }}^*\) can slightly vary. In order to do this, we set a constant \(\rho > 0\) and define the open ball

$$\begin{aligned} B({\boldsymbol{\lambda }}^*,\rho ) = \{{\boldsymbol{\lambda }}\in \mathbb {R}^m \,|\, \left\| {\boldsymbol{\lambda }}- {\boldsymbol{\lambda }}^*\right\| < \rho \}, \end{aligned}$$
(11)

where \(\left\| \cdot \right\| \) is the Euclidean norm defined in Sect. 2.1.

We start by recalling the Monte Carlo procedure for estimation. This procedure aims at taking advantage of the Central Limit Theorem and the Law of Large Numbers. In order to estimate the probability that our system (where \({\boldsymbol{\lambda }}\) can vary inside of \(B({\boldsymbol{\lambda }}^*,\rho )\)) satisfies the given BLTL property \(\varPsi ^*\) (see Eq. (5)), we will generate a set of n samples of values for \({\boldsymbol{\lambda }}\) inside of \(B({\boldsymbol{\lambda }}^*,\rho )\), and use these values to provide n solutions to the ODE system. Each solution will be evaluated, yielding a score of 1 if it satisfies \(\varPsi ^*\) and 0 otherwise. Informally, the Central Limit Theorem (Theorem 1) states that the mean value of the samples \(\hat{p}\) is a good estimator for the probability p that our system (i.e. the ODE system, where the parameter value is set to \({\boldsymbol{\lambda }}^*\), with internal variability) satisfies \(\varPsi ^*\). Moreover, it also provides a confidence interval that solely depends on the number of samples—provided this number is large enough—and the variance of the initial distribution.

Theorem 1

(Central Limit Theorem [19]). Let \(X_1,X_2,\dots \) be a sequence of independent and identically distributed random variables of mean \(\mu \) and variance \(\sigma ^2\). Then, the distribution of \(\frac{\sum _{i = 1}^n X_i - n\mu }{\sigma \sqrt{n}}\) tends to the standard normal distribution as \(n \rightarrow \infty \). That is, for any \(a \in \mathbb {R}\),

$$\begin{aligned} \lim _{n \rightarrow \infty } \mathbb {P}\left( \frac{\sum _{i = 1}^n X_i - n\mu }{\sigma \sqrt{n}} \le a \right) = \frac{1}{\sqrt{2\pi }}\int _{-\infty }^a e^{-x^2/2} dx. \end{aligned}$$

Because we cannot evaluate the exact solutions of the ODE system but instead have to rely on approximate solutions, we will define two auxiliary properties \(\varphi _1^\varepsilon \) and \(\varphi _2^\varepsilon \) (not expressed in BLTL) that take into account the global approximation error defined above, use the Monte Carlo procedure to estimate two probabilities \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \) using those properties and the approximate solutions, and finally propose an estimation of \(\hat{p}\) that relies on \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \). We will finally use \(\hat{p}\) in order to rate the chosen (central) parameter value \({\boldsymbol{\lambda }}^*\).

Let \(\mathcal {T}\) be a set of time points as described earlier. Let \(\gamma \) be the set of experimental data and \(\delta >0\) be a precision (tolerance) w.r.t. \(\gamma \). Let \({\boldsymbol{\lambda }}^* \in \textbf{W}\) be a parameter value, let \(\rho >0\) be a variability setting. Consider the ball \(\mathcal {B}_{{\boldsymbol{\lambda }}^*}= B({\boldsymbol{\lambda }}^*,\rho )\) and let \(\mathbb {P}^{{\boldsymbol{\lambda }}^*}\) be the uniform distribution on this ball.

Given a function \(g \in F_\mathcal {T}\), we write \(\varphi (g) := d(g,\gamma ) \le \delta \) the property that means “the distance between g and \(\gamma \) is less than \(\delta \)”. Note that this property can easily be written in BLTL (see Eq. (5) above). For convenience, if \(y^{\boldsymbol{\lambda }}\) is an approximate solution to Eq. (1) induced by the parameter \({\boldsymbol{\lambda }}\in \mathcal {B}_{{\boldsymbol{\lambda }}^*}\), we will identify \(\varphi ({\boldsymbol{\lambda }})\) to \(\varphi (y^{\boldsymbol{\lambda }})\).

Given \(\varepsilon > 0\), we introduce the properties:

$$\begin{aligned} \begin{aligned} \varphi (z^{\boldsymbol{\lambda }}) := d(&z^{\boldsymbol{\lambda }}, \gamma ) \le \delta ,\\ \varphi _1^\varepsilon (y^{\boldsymbol{\lambda }}) := d(y^{\boldsymbol{\lambda }}, \gamma ) + \varepsilon \le \delta , \quad&\varphi _2^\varepsilon (y^{\boldsymbol{\lambda }}) := d(y^{\boldsymbol{\lambda }}, \gamma ) - \varepsilon \le \delta . \end{aligned} \end{aligned}$$

The translation of \(\varphi \) in BLTL is the property of interest \(\varPsi ^*\) defined in Eq. (5). Our aim is to provide an estimation \(\hat{p}\) for \(\mathbb {P}^{{\boldsymbol{\lambda }}^*}(\varPsi ^*)\). For convenience, we write \(\mathbb {P}\) for \(\mathbb {P}^{{\boldsymbol{\lambda }}^*}\) in the rest of this section.

In order to do that, we show in Lemma 1 that for a small enough integration step h, we have \(\epsilon _h({\boldsymbol{\lambda }}) \le \varepsilon \) for all \({\boldsymbol{\lambda }}\in \mathcal {B}_{{\boldsymbol{\lambda }}^*}\), and therefore

$$\begin{aligned} \varphi _1^\varepsilon (y^{\boldsymbol{\lambda }}) \Rightarrow \varphi (z^{\boldsymbol{\lambda }}) \Rightarrow \varphi _2^\varepsilon (y^{\boldsymbol{\lambda }}). \end{aligned}$$
(12)

Lemma 1

Let \((h_i)_{i \in \mathbb {N}} \in \mathbb {R}^+ \) be a sequence of integration steps, such that \(\lim \limits _{i \rightarrow \infty } h_i = 0\). Then for all \(\varepsilon > 0\), there exists \(i^* > 0\) such that

$$\begin{aligned} \epsilon _{h_i}({\boldsymbol{\lambda }}) < \varepsilon , \quad \forall i \ge i^*, \forall {\boldsymbol{\lambda }}\in \mathcal {B}_{{\boldsymbol{\lambda }}^*}. \end{aligned}$$
(13)

In other words, the global error \(\epsilon _h({\boldsymbol{\lambda }})\) can be uniformly bounded in the closure \(\overline{\mathcal {B}_{{\boldsymbol{\lambda }}^*}}\) of the open ball \(\mathcal {B}_{{\boldsymbol{\lambda }}^*}\). The proof of this lemma is given in Appendix A, along with a method to compute \(h_{i^*}\).

Now, we define the probabilities

$$\begin{aligned} p = \mathbb {P}\big (\varphi (z_{{\boldsymbol{\lambda }}^*})\big ), \quad p_1^\varepsilon = \mathbb {P}\big (\varphi _1^\varepsilon (y_{{\boldsymbol{\lambda }}^*})\big ), \quad p_2^\varepsilon = \mathbb {P}\big (\varphi _2^\varepsilon (y_{{\boldsymbol{\lambda }}^*})\big ). \end{aligned}$$
(14)

Note that p, \(p_1\), \(p_2\) implicitly depend on \(\delta \). However, we omit this dependence in order to lighten our notations. Next, it is straightforward that

$$\begin{aligned} p_1^\varepsilon \le p \le p_2^\varepsilon , \quad \forall \varepsilon > 0. \end{aligned}$$
(15)

Estimators \(\hat{p}_1^\varepsilon \), \(\hat{p}_2^\varepsilon \) of the probabilities \(p_1^\varepsilon \) and \(p_2^\varepsilon \) respectively can be determined using the Monte-Carlo procedure, involving a precision \(\alpha \) and a risk \(\theta \). Our main result, given in Theorem 2 below, establishes a statistical guarantee on the probability p of interest with respect to these estimators \(\hat{p}_1^\varepsilon \), \(\hat{p}_2^\varepsilon \).

Theorem 2 (Main theorem)

Let \({\boldsymbol{\lambda }}^* \in \textbf{W}\), \(\rho > 0\), \(\delta > 0\), \(\varepsilon > 0\). For any risk \(\xi \in (0, 1)\), we define \(\theta = 1 - \sqrt{1 - \xi }\). Then, for any precision \(\alpha > 0\), the probabilities \(p_1^\varepsilon \) and \(p_2^\varepsilon \) defined in Eq. (14) satisfy

$$\begin{aligned} \mathbb {P}\big (p_1^\varepsilon \in [\hat{p}_1^\varepsilon - \alpha , \hat{p}_1^\varepsilon + \alpha ] \big ) \ge 1 - \theta , \quad \mathbb {P}\big (p_2^\varepsilon \in [\hat{p}_2^\varepsilon - \alpha , \hat{p}_2^\varepsilon + \alpha ] \big ) \ge 1 - \theta , \end{aligned}$$
(16)

where the estimators \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \) can each be determined after performing a number \(N' = \frac{\log (2/\theta )}{2\alpha ^2}\) (and hence a total number \(N = 2 \times \frac{\log (2/\theta )}{2\alpha ^2}\)) of simulations of Eq. (1) induced by parameter values \({\boldsymbol{\lambda }}\) sampled in \(\mathcal {B}_{{\boldsymbol{\lambda }}^*}\).

Furthermore, there exist \(\varepsilon _0 > 0\) and \(h_0 > 0\) sufficiently small such that, for any integration step \(h \le h_0\) and any \(\varepsilon < \varepsilon _0\), the following statements hold:

  • the probability p defined in Eq. (14) satisfies the estimation

    $$\begin{aligned} \mathbb {P}\big ( p \in [\hat{p}_1^\varepsilon - \alpha , \hat{p}_2^\varepsilon + \alpha ] \big ) \ge 1 - \xi , \end{aligned}$$
    (17)

  • the distance between \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \) satisfies:

    $$\begin{aligned} \mathbb {P}\left( \left| \hat{p}_1^\varepsilon - \hat{p}_2^\varepsilon \right| \le 3\alpha \right) \ge 1 - \xi . \end{aligned}$$
    (18)

We emphasize that estimations (17) and (18) imply a confidence interval of width \(5\alpha \) for p and require a number of samples \(N = 2 \times \frac{\log (2/\theta )}{2\alpha ^2}\). If the analysis was performed directly on the exact solutions of the ODE, we would have a confidence interval of width \(2\alpha \) and only require \(\frac{\log (2/\xi )}{2\alpha ^2}\) samples.

The proof of Theorem 2, given in Appendix B, is divided in three main steps. First, using the Central Limit Theorem and the Law of Large Numbers, we determine estimators \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \) of \(p_1^\varepsilon \) and \(p_2^\varepsilon \), respectively. Then, Eq. (14) and the independence of simulations lead to the confidence interval of p. Finally, Lemma 1 guarantees that proper values of h and \(\varepsilon \) can be found, in order to control the distance between \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \). It is worth noting that, for some resolution methods (such as Runge-Kutta 4 for example), a value for h can be explicitly determined to guarantee Lemma 1 for a given \(\varepsilon \) and therefore Eq. (17). However, the convergence speed of \(\left| \hat{p}_1^\varepsilon - \hat{p}_2^\varepsilon \right| \) is not known in general, therefore we can only guarantee the existence of a sufficiently small value for \(\varepsilon \) to ensure Eq. (18) but not compute it.

3.3 Model Checking Extension Through Reward Functions

As explained in Sect. 2.3, our method can be extended to non-Boolean reward functions. Indeed, these functions may provide not only qualitative results—“does the property hold?”—but also quantitative ones—“how well does the property hold?”. In our case, this allows to distinguish the good parameters that induce a suitable solution from the best ones that induce the solutions closest to the data.

To use such a real-valued reward function r, some conditions are required. First, it must be assumed that two other reward functions \(r_1\) and \(r_2\) can be found, such that the following estimation holds for any \({\boldsymbol{\lambda }}\in \mathcal {B}_{{\boldsymbol{\lambda }}^*}\):

$$\begin{aligned} r_1({\boldsymbol{\lambda }}) \le r({\boldsymbol{\lambda }}) \le r_2({\boldsymbol{\lambda }}). \end{aligned}$$
(19)

Second, the law of the unconscious statistician must be applicable to these lower and upper reward functions, i.e. the computation of the expected valueFootnote 2 must be applicable, so that estimators \(\hat{r}_1\) and \(\hat{r}_2\) of \(r_1\) and \(r_2\) respectively, can be computed.

Moreover, and most importantly, the reward function must be compatible with the global error defined in Eq. (10). Indeed, since we compute score based on approximated solutions, said computations must take this approximation into account to provide any significance to the resulting score. It is worth noting that these conditions are satisfied by all the reward functions we have considered in this work, such as the total accumulated/maximal/average distance to \(\gamma \) or the number of time points where \(\gamma \) is not respected.

Similarly to Eq. (18), the distance between \(\hat{r}_1\) and \(\hat{r}_2\) must be controlled. Depending on the order of the approximation method used to compute approximate solutions to the ODEs, this may be easy to ensure. For instance, in our case the integration method Runge-Kutta 4 ensures that the approximation error—and thus, the global error as defined in Eq. (10)—is of order 5: all derivatives of the integration functions converge at most linearly w.r.t. \(h^5\), where h is the integration step.

4 Case Studies

In this section, we apply our method to two case studies [17, 22] taken from the literature to show its potential. After presenting the studies and their results, we will display our results and discuss them. We implemented our technique in C++ to validate the approach. The experiments were realized on a 2.1 GHz Intel Xeon Silver 4216 processor, running g++ version 7.5.0 on Ubuntu 18.04. The code is available at https://gitlab.com/davidjulien/smc_for_ode.git, and the experiments can be reproduced using the right branches, i.e. compute_aurelia to run the experiment from Sect. 4.1 and compute_prey to run the experiment from Sect. 4.2. We used the Runge-Kutta 4 method to compute approximate solutions, a SMC precision \(\alpha =0.05\) and a risk \(\xi = 0.05\).

First, we briefly recall the experiment. After discretizing the value space \(\textbf{W}\) defined in Eq. (2) for the parameter \({\boldsymbol{\lambda }}\), we will grade every value in order to select the best ones w.r.t. the experimental data \(\gamma \). In order to take the internal variability of the model into account, each chosen parameter value \({\boldsymbol{\lambda }}^*\) is associated with the open ball \(\mathcal {B}_{{\boldsymbol{\lambda }}^*}\) as defined in Eq. (11). Once the SMC parameters \(\alpha \) and \(\xi \), as well as a small enough value for \(\varepsilon \) are chosen, we can compute an integration step h, as well as a required number N of samples such that Theorem 2 holds. Then, we sample N values \({\boldsymbol{\lambda }}\in \mathcal {B}_{{\boldsymbol{\lambda }}^*}\), compute the approximated solutions to the induced ODEs, and compare them with the experimental data \(\gamma \). For each \({\boldsymbol{\lambda }}^* \in \textbf{W}\), we thus estimate the probabilities \(\hat{p}^{\varepsilon }_1\) and \(\hat{p}^{\varepsilon }_2\) defined in the previous section, and use them to define \(\textsf{grade}({\boldsymbol{\lambda }}^*) = \frac{\hat{p}^{\varepsilon }_1 + \hat{p}^{\varepsilon }_2}{2}\). In order to better discriminate the best parameter values, we also estimate the expected value of the reward function \(r : {\boldsymbol{\lambda }}\mapsto d(z_{\boldsymbol{\lambda }},\gamma )\) that measures the distance between the ODE simulations and the experimental data.

4.1 Case Study 1: A Study on Aurelia Aurita Population Growth [17]

In 2014, Melica et al. [17] published a paper studying the growth of Aurelia Aurita, a species of jellyfish that is very common in Adriatic Sea. In this paper, they compared experimental data, resulting from the culture of Aurelia Aurita polyps, to simulation models based on the following ODE:

$$\begin{aligned} x'(t) = ax(t)(1 - x(t)/b) \end{aligned}$$
(20)

where t is time, x is the population density, a is the maximum rate of population growth, and b is the positive equilibrium. The authors show that the dynamics of a Aurelia Aurita polyps population can, indeed, be modeled by the density-dependent, or Verhulst [23], ODE presented above and compute the values for a and b that ensure the best fitting w.r.t. the experimental data. These values are recalled in Table 1.

Table 1. Estimation of parameters of the logistic curve fitting the laboratory experimental data [17].
Full size table

Remark 1

HD and LD represent the studies for High and Low Density, respectively, which were both ran by the original authors. Here, we focused on the High Density case.

In order to illustrate our method, we applied it to the same case study, using Eq. (20) as the ODE system. We evaluated parameter values in the ranges \(a \in [0,3], b \in [0,9]\), and discretized this space with a parameter step of 0.01. We set the internal variability of the parameters \(\rho = 0.005\) and performed \(N = 874\) simulations for each parameter value on the discretized space, therefore ensuring a statistical precision of \(\alpha = 0.05\) and risk of \(\xi = 0.05\).

Fig. 3.
figure 3

Heatmap of the score of the parameters. (Color figure online)

Full size image
Fig. 4.
figure 4

Heatmap of the distance to \(\gamma \). (Color figure online)

Full size image
Fig. 5.
figure 5

Solution to the ODE from Eq. (20). (Color figure online)

Full size image

In Fig. 3, we represent the score of the best parameter values, where the white zones are zones where \(\textsf{grade}({\boldsymbol{\lambda }}^*) = 0\). One can see that there is a small gradient in the area where the score is positive, but this is not enough to discriminate between the parameter values in this zone. In order to refine the result, we present in Fig. 4 the estimation of the expected value of the reward function \(r : {\boldsymbol{\lambda }}\mapsto d(z_{\boldsymbol{\lambda }},\gamma )\). Figure 4 shows a tighter area of values that induce solutions that are very close to the data (down to 0.50 polyps on average), plotted in red, which contains the parameter value estimated by [17]: it comforts us in saying that our method provides tangible results. The best parameter found using our method is the pair \((a,b) = (0.19, 5.57)\). It induces the red curve in Fig. 5.

4.2 Case Study 2: A Prey-Predator Model for Lynx and Hares [22]

In 2010, Restrepo and Sánchez [22] published a paper describing a genetic algorithm, which aimed at estimating the best parameters for prey-predator models. The first model, which we will study in the following, is a basic prey-predator interaction model defined by the following ODE system:

$$\begin{aligned} P' = a P - b {PD}, \quad D' = -c D + d {PD} \end{aligned}$$
(21)

where t is time, P and D are the two time-dependent variables representing the quantity of individuals in each group: P(t) for prey and D(t) for predators; a, b, c, d are positive constants, a and c indicating the birth rate of prey and death rate of predators respectively, and b and d representing the rates of predation and reproduction of predators. Note that even if the model is a standard way to describe, on first approximation, such an interaction between two populations, its simplicity might make it imprecise – which is why other, more complex models are studied in [22]. The best values for parameters (a, b, c, d) w.r.t. experimental data are given in [22]: \((a,b,c,d) = (0.55,0.027,0.83,0.026)\).

Again, we applied our method to this case study, using Eq. (21) as the ODE system. We evaluated parameter values in the ranges \(a \in [0.48,0.68]\), \(b\in [0.015;0.04]\), \(c \in [0.78, 0.9]\), \(d \in [0.01,0.05]\), and discretized this space with a parameter step of 0.001. We set the internal variability of the parameters \(\rho = 0.0005\) and performed \(N = 874\) simulations for each parameter value on the discretized space, therefore ensuring a statistical precision of \(\alpha = 0.05\) and risk of \(\xi = 0.05\). Note that the parameter ranges have been tightened according to the paper results, since cyclic models can be very sensitive to parameter values.

Fig. 6.
figure 6

Heatmap of the score (for \(c = 0.89\)).

Full size image
Fig. 7.
figure 7

Heatmap of the distance to \(\gamma \) (for \(c =0.89\)).

Full size image
Fig. 8.
figure 8

Best solution to Eq. (21).

Full size image

We encountered two issues with this study. First, the adequacy of the model with the data was improvable, thus computing a fitting solution was challenging. We had to loosen the property we verify: instead of \(\varPsi ^*\), which enforces the solution to always stay in the tunnel, we verified a property \(\varPsi ^\dag \), which allows the solutions to step out of the tunnel a total of 5 times (for a total of 22 time points) before rejecting them. This explains why the best solution displayed in Fig. 8 does not perfectly fit inside of the tunnel. Remark that \(\varPsi ^\dag \) can easily be expressed in BLTL, and is therefore compatible with our theory. Second, since system Eq. (21) involves 4 parameters, displaying the results with heatmaps is more difficult than in case study 1 (Sect. 4.1). Nonetheless, locking a parameter value (here, \(c = 0.89\)) allows the plot of a 3-dimensional heatmap.

Figure 6 shows a local subset of solutions fitting the data with a certain quality. Notice that the score only goes up to 0.5; because of the internal variability we impose and the sensitivity of the model, very few simulations stayed in the inner tunnel (corresponding to \(\varphi ^\varepsilon _1\) in Sect. 3), yielding \(\hat{p}^\varepsilon _1 = 0\) in most cases. That said, Fig. 7 displays the distance for the same subset. We notice that some solutions are, at most, at a 10 individuals distance from the data. The subset contains our best candidate \((a,b,c,d) = (0.52,0.027,0.89,0.027)\), whose corresponding curve is displayed in Fig. 8. We see that the general shape of the curve is satisfying but does not perfectly fit inside of the tunnel. This may be explained by the fact that cyclic ODE systems like prey-predator models can be very sensitive to the non-linear terms, i.e. bPD and dPD. Again, our goal here was to prove the concept rather than describe a phenomenon with the upmost precision: while this is satisfying as far as we are concerned, a more thorough study of the parameters, along with a better quality of the data (with e.g. several observations for each time point t, allowing for more robust data and observable data tunnels) would help getting results closer to the actual experiments.

5 Conclusion

In this paper, we have proposed a statistical method for synthesizing the best parameter values w.r.t. given experimental data for an ODE system with internal variability, while providing formal statistical guarantees that for the first time (to the best of our knowledge) take into account the approximation error introduced through the numerical resolution of the ODEs. To do that, we discretize the parameter space and define balls around the resulting (finite) set of parameter values to take internal variability into account. We then use the Monte-Carlo technique to estimate the probability that exact solutions of the ODE system are close to the experimental data for each resulting parameter ball, and use the result of this estimation to select the best (central) parameter values. Our main contribution is Theorem 2 which guarantees the precision of our estimation despite the fact that it is performed using numerical resolution techniques that do not give us access to exact solutions of the ODE system. In contrast with other existing works on parameter estimation for ODE systems, like [15], where this problem is left aside, we show that the number of simulations required for a given precision and risk of the statistical estimation is (more than) twice the one needed when working with exact solutions. We also show that an upper bound on the integration step of the chosen integration technique exists (and can be computed for standard integration techniques) in order to make sure that a given statistical precision and risk are respected.

One of the limitations of our work is that, in order to prove our results and perform parameter synthesis in practice, we rely on a setting \(\varepsilon \) that represents the maximal admissible distance between exact and approximate solutions to the ODE system. Although it is possible, for most integration techniquesFootnote 3, to compute an integration step that will guarantee that a given value for \(\varepsilon \) is respected, our results only show the existence of a suitable value for \(\varepsilon \) for any statistical setting, but do not provide any method to compute this value in practice. This is due to our lack of guarantees on the convergence speed of the distance between the two estimators \(\hat{p}_1^\varepsilon \) and \(\hat{p}_2^\varepsilon \) that appear in Eq. (17) and Eq. (18). What we do in practice is that we set small values for \(\varepsilon \), perform experiments and then estimate the value of \(|\hat{p}_1^\varepsilon - \hat{p}_2^\varepsilon |\). If the resulting value is too large, then we start over the experiment with a smaller value for \(\varepsilon \).

Although the only BLTL property that we verify in this paper is the property \(\varPsi ^*\) defined in Eq. (5), we believe that our reasoning can be easily extended to other BLTL property following the definition given in Sect. 2.2. This is, in our opinion, a straightforward extension that we will address in the near future.

As said in the introduction, our results are generic and could therefore be combined with any exploration strategy for the parameter space. The global exploration we perform in this paper is obviously costly but yields global information that is precious when analysing a complex system. In the future, we plan on combining a coarse global exploration to identify interesting zones in the parameter space with more efficient and detailed search algorithms (such as the one from [15]) limited to those zones.