The behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to uncertainties. We propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Distribution Temporal Logic (DisTL), a novel temporal logic allowing us to specify properties on the expected behaviour of systems, and to include the presence of uncertainties in the specification. We equip DisTL with a robustness semantics and we prove it sound and complete w.r.t. the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we give a statistical model checking algorithm for DisTL specifications, and we apply our framework to a simple unmanned ground vehicle scenario.
We have recently proposed a formal framework to model and analyse the behaviour of systems
that are subject to uncertainty. The most prominent example is that of cyber-physical systems [
Then, we have introduced, in [
The expressive power of RobTL comes at a price: besides the behaviour of the agents and the
environment, we must be able to specify the perturbation that afects the system, in order to
measure its robustness. While our tool Stark, the Software Tool for the Analysis of Robustness in
the unKnown environment [
Our Contribution: The Distribution Temporal Logic Let us consider a simple scenario: an unmanned ground vehicle is proceeding on a straight path towards a toll booth (henceforth, the objective), where it has to stop to allow the passenger to retrieve the entry ticket to the motorway. With classic probabilistic temporal logics (like, e.g., PCTL [13], CSL [14, 15], probabilistic variants of LTL [16], and probabilistic variants [17, 18] of MTL [19] and STL [20]), we can verify whether the vehicle is going to stop within a certain distance from the objective, and/or whether the probability to do so is above/below a desired threshold. We remark that this is achieved by reasoning in a trace-by-trace fashion: first we check the property over each trajectory of the system, and then we sum up the probability weights of those satisfying it.
Here we want to perform a diferent analysis: due to the presence of uncertainties, it would be preposterous to require the vehicle to stop precisely at the objective. Our aim is to express that the vehicle is expected to stop there, and to allow a certain variance on its actual final position, to take uncertainties into account, while guaranteeing that hazardous behaviours are avoided. Technically speaking, we want to specify that, when considering all possible system behaviours, the final (i.e., stationary) position of the vehicle agrees with a desired distribution, like, e.g., a Gaussian centred over the objective.
To this end, we introduce the Distribution Temporal Logic (DisTL), a novel temporal logic
allowing us to express requirements on the expected behaviour of the system in the presence of
uncertainties and perturbations, by using distributions over data states as atomic propositions.
We equip DisTL with a real-valued semantics expressing the robustness of the satisfaction of
DisTL specifications. The robustness of a system s with respect to a formula is expressed as a
real number J Ks ∈ [
In order to show how our techniques can be applied, we consider the unmanned ground vehicle scenario described above as a case study.
Evolution Sequences We consider systems consisting of a set of agents and an environment, whose interaction produces changes on a shared data space , containing the values assumed by variables, representing: (i) physical quantities, (ii) sensors, (iii) actuators, and (iv) internal variables of the agents. Technically, we assume a finite set of variables Var such that for each ∈ Var the domain ⊆ R is either finite , or a compact subset of R. Notice that, in particular, this means that is a Polish space. Moreover, as a -algebra over we assume the Borel -algebra, denoted ℬ. The data space over Var is then defined as the Cartesian product over the variables domains = × ∈Var , and it is equipped with the product -algebra ℬ = ⨂︀∈Var ℬ [22].
We call data state the current state of the data space, and represent it by a mapping d : Var →
R, with d() ∈ for all ∈ Var. At each step, the agents and the environment induce some
changes on the data state, providing a new data state at the next step. Those modifications are
also subject to the presence of uncertainties, meaning that it is not always possible to determine
exactly the values assumed by data at the next step. Hence, following [
Definition 1 (Evolution sequence, [
∫︁ +1(D) =
step(d)(D) d (d).
We denote by S the set of all possible evolution sequences over .
A Distance on Evolution Sequences We introduce a distance measuring the diferences in
the behaviour of systems that will be used to define the robustness of DisTL specifications. The
idea is first to introduce a distance on distributions over data states measuring their diferences
with respect to a given target, and then to extend it to the evolution sequences. Following [
We have implemented a simple language, PF, to model penalties in Stark:
Definition 2 (Penalties). Penalties in PF are defined as follows:
pf ::=
0
|
where pf ranges over PF, and are finite natural numbers, and:
• 0 is the null penalty, i.e., at each time step it assigns penalty 0 to any data state;
• f@ is an atomic penalty, i.e., a function f : → [
This simple language allows us to define some non-trivial penalties that we can use to analyse systems behaviour, like in the following example designed for our case study: Example 1. As the task of the vehicle is to stop at the objective, it is natural to use the normalisation of its distance from it, stored in variable p_dist, as a penalty. However, we notice that since the distance changes in time, in order to have a meaningful penalty value we also need to change the normalisation factor. In fact, if, for instance, we normalise only with respect to the initial distance, the penalty is fated to decrease in time, and thus we may loose important information on the behaviour of the vehicle when it gets closer to the objective. Therefore, assuming that the vehicle is at an initial distance from the objective of 10000 m, we consider the following penalty: f(d) = d(p_dist) .
Each pf ∈ PF denotes a penalty function of type × N → [
We can now define the semantics of penalties as the mapping ⟨·⟩ : PF → ( × N → [
⟨pf⟩(d, ) = effect(next(pf))(d), where next0(pf) = pf and next(pf) = next(next− 1(pf)), for all > 0.
The next proposition follows directly from the definition of the mapping ⟨·⟩ . Proposition 1. For each pf ∈ PF, the mapping ⟨pf⟩ is a penalty function.
Then we use penalty functions to obtain a distance on data states:
Definition 3 (Metric on data states). Let : × N → [
m (d1, d2) = max{ (d2) − (d1), 0}.
Wasserstein lifting of m to a distance between and is defined by we make use of the Wasserstein lifting [21]: for any two distributions ,
Note that m (d1, d2) is a hemimetric expressing how much d2 is worse than d1 according to . Then, we need to lift the hemimetric m to a hemimetric over Δ(, ℬ). To this end, on (, ℬ), the ∫︁ W(m )(, ) = inf
m (d, d′) dw(d, d′) w∈W(, ) × on the definition of the Wasserstein lifting over hemimetrics.) where W(, ) is the set of the couplings of and , namely the set of joint distributions w over the product space ( × , ℬ( × )) having and as left and right marginal, respectively, i.e., w(D × ) = (D) and w( ×
D) = (D), for all D ∈ ℬ(). (See [
EmOT : S × S → [
Definition 4 (Evolution metric). Assume a finite set OT of time steps, a penalty function and the metrics on data states m . Then, the evolution metric over and OT, is the mapping EmOT(1, 2) = max W(m )(1, , 2, ).
∈OT
We remark that since we are interested in verifying requirements over a finite horizon (and we use only bounded temporal operators in the logic), the choice of having OT finite is not too restrictive.
As a running example, we consider the unmanned ground vehicle scenario described in the Introduction. Since our objective is merely to showcase the features of the new logic, we work under the following simplifying assumptions: 1. All the objects on the scene, including the vehicle, are one-dimensional; 2. When we start the simulation, the (program controlling the) vehicle already knows its distance from the point at which it has to stop (i.e., its distance from the button on the toll booth, henceforth referred to as the objective); 3. The acceleration of the vehicle can assume two values: a positive one A m/s2, and a negative one -B m/s2 (with B> 0); 4. The vehicle is equipped with a speed sensor, s_speed, that is subject to uncertainty (related to instrument accuracy); 5. The speed can never be negative (i.e., we do not allow the vehicle to shift into reverse). Every TIMER steps, the vehicle decides whether to accelerate or brake, according to the sensor readings and its distance from the objective.
To specify the details of the behaviour of the vehicle we use our tool Stark. The vehicle is modelled as a Stark component, consisting of a set of local variables, used to allocate sensor readings and the value of the acceleration actuator, and a Stark controller, i.e., the process rendering the behaviour of the vehicle. Due to space limitations, we give only an informal presentation. The interested reader can find the full Stark specification at https://github.com/ quasylab/jspear/tree/Tony. The behaviour of the controller is specified by means of four processes, or states: Ctrl, Accelerate, Decelerate and Stop. The computation starts from Ctrl that checks, every TIMER steps, whether the vehicle can accelerate or if it has to brake, and sets the acceleration actuator accordingly. The decision is taken on the basis of the sensed speed and the distance from the objective. States Accelerate and Decelerate manage, respectively, the acceleration and braking phases: the vehicle maintains a constant acceleration (of A m/s2 in the case of Accelerate, and of -B m/s2 for Decelerate), for TIMER steps; then Ctrl is woken up for a new check. When the speed becomes zero, and it is not possible to get closer to the objective, process Stop sets the acceleration actuator to 0 m/s2, and the vehicle becomes stationary.
To model the evolution of the scenario we use a Stark environment, that allows us to set the position of the objective, and to model the movement of the vehicle towards it. In this simple scenario, the uncertainty in the model is given by the precision error in the readings of sensor s_speed. Hence, we include a random noise in the updates of that value made by the environment.
We now introduce the Distribution Temporal Logic (DisTL) which allows us to specify
requirements on the expected behaviour of the system, in the presence of uncertainties and perturbations.
The logic bases on two atomic properties, target( ) and brink( ) , where is a distribution
over data states in (, ℬ), is a penalty function and is a real in [
Conversely, in the formula brink( ) the distribution expresses some unwanted, hazardous, behaviour. Hence, the distribution reached by the system must be better than , i.e., W(m )( , ) > 0. Also in this case, due to the presence of uncertainties, we need to make use of a threshold parameter : assuming a distribution acceptable when it is only slightly better than can still lead to an unwanted behaviour (because, in this case, the diference between the two distributions may be due only to some noise). Hence, we let be the minimal required distance between and , so that is an acceptable behaviour if and only W(m )(, ) = 0. Instead, we if W(m )( , ) ≥ .
Let var( ) ⊆
Var be the set of data variables over which the distribution is defined.
Similarly, for a penalty function , we can consider the set var( ) ⊆
following syntax:
Definition 5 (DisTL). The modal logic DisTL consists in the set of formulae ℒ defined by the
::= ⊤ | target( )
| brink( )
| ¬ | ∨ | 1
that var( ) ⊆ var( ), ∈ [
Disjunction and negation are the standard Boolean connectives, and 1 bounded until operator stating that 1 is satisfied until, at a time in [, ], 2 is. As expected, [,] 2 is the other standard operators can be defined as macros in our logic: 1 ∧ 2 ≡ ¬ (¬ 1 ∨ ¬ 2) ♢ [,] ≡ ⊤ [,] 2 □ [,] ≡ ¬ ♢ [,] .
¬
Formulae are evaluated over evolution sequences and time steps. In a quantitative semantics approach, for a formula , an evolution sequence , and a time step , the value expresses the robustness of with respect to at time , i.e., how much the behaviour can be modified, either while preserving the validity of property (if is already satisfied), or in J
K, ∈ [
target( )
J⊤K, = 1
K, = − Jbrink( ) K, = W(m )( , ) −
W(m )(, )
J¬ K, = − J K,
J 1 ∨ 2K, = max {J 1K, , J 2K, } J 1 [,] 2K, =
max ′∈[ +, +] min {︁ J 2K, ′ , ′′∈[ +, ′)J 1K, ′′ }︁.
min
Intuitively, the value W(m )(, ) quantifies the diference between the distribution reached by the system at time and . Hence, on the one hand the robustness Jtarget( ) K, expresses whether the distribution in the evolution sequence of s is within the maximal acceptable distance from . On the other hand, it also expresses how much can be modified while guaranteeing that the behaviour of the system remains within the specified parameters. Clearly, the closer and , the higher the robustness. Similarly, Jbrink( ) robustness with respect to (and ) in terms of how much may get close to while keeping the minimal required distance . Hence, the farther and , the higher the robustness. The semantics of boolean connectives and bounded until is standard. Notice that due to the potential K, quantifies the asymmetry of our distances, it is not true in general that brink( ) = ¬target( )1−
Example 2. Let us now use DisTL to formalise the requirement on the final position of the vehicle discussed at the beginning of this section: we want to express that it is distributed like a Gaussian centred on the objective and with variance 2, for some . In the Stark implementation of the system, the position of the vehicle is modelled in terms of its physical distance from the objective: when variable p_dist equals 0, the position of the vehicle corresponds to the objective. Hence, we can use as the target distribution over the position. Given the penalty pos defined in Example 1, and a desired tolerance , we can use the formula
pos = p_dist ∼ (0, 2) 1 = □ [ 1, 2]target( pos)pos to capture the requirement on the final position, where the time interval [ 1, 2] is chosen according to the systems parameters.
Clearly, we can use DisTL also to express strict requirements (i.e., without approximations and tolerances): for instance, we must require that the vehicle is stationary in the final position, i.e., that its speed equals 0. This can be done by means of a Dirac (or point) distribution 0(p_speed), henceforth denoted sp, where p_speed is the variable storing the value of the physical speed of the vehicle. Consider the penalty function
sp(d) = (d(p_speed)/MAX_SPEED@0)h, where MAX_SPEED is the parameter storing the maximal speed of the vehicle. We can then use the atomic formula target( sp)0sp to express that the speed of the vehicle must be 0 (notice the tolerance 0). Then, we can combine the two formulae to express that the vehicle is expected to stop in an -neighbourhood of the objective, within a time horizon h (determined according to the other parameters of the system, like TIMER, A, and B): 2 = ♢ [0,h] (︀ target( sp)0sp ∧ target( pos) pos )︀ . form (· )(· ).
We can show that DisTL characterises the distance between evolution sequences. More precisely, the quantitative semantics of DisTL induces a distance between evolution sequences that coincides with the symmetrisation of the hemimetric EmOT and is therefore a pseudometric. Clearly, since the evolution metric is defined in terms of a given penalty function , it will be characterised by the distance over formulae in ℒ , which is the sub-class of ℒ with atomic propositions of the penalty function and OT is defined as Definition 7 (DisTL distance). The DisTL distance between 1, 2 ∈ S with respect to a LOT(1, 2) = ∈ℒ , ∈OT |J K1, − J K2, | .
sup
Firstly, we show that the symmetrisation of EmOT is an upper bound to LOT. for some ∈ OT. of EmOT coincide.
From Lemma 1 and Lemma 2 we infer that the DisTL distance LOT and the symmetrisation
LOT(1, 2) ≤
max {︀ EmOT(1, 2), EmOT(2, 1)︀} . 1, 2.
Then, we show that for all evolution sequences 1, 2 there exists a formula in ℒ such that the symmetrisation of EmOT coincides with the diference in the evaluations of over Lemma 2. For all 1, 2 ∈ S and penalty functions , there is a formula ∈ ℒ with |J K1, − J K2, | = max {︀ EmOT(1, 2), EmOT(2, 1)︀} ,
LOT(1, 2) = max {︀ EmOT(1, 2), EmOT(2, 1)︀} .
respect to is positive as well.
Theorem 1 entails the soundness (Lemma 1) and completeness (Lemma 2) of our notion of robustness. In particular, as a direct consequence of Theorem 1, we can obtain the following classic result (see, e.g., [24]): whenever the robustness of a evolution sequence with respect to a formula is greater than the distance between and ′, then the robustness of ′ with max {︀ EmOT(1, 2), EmOT(2, 1)︀} , then J K3− , ≥ 0.
Corollary 1. Let be any formula in ℒ , ∈ OT and let ∈ {1, 2}. Whenever J K, ≥
{d21, . . . , dℓ2 } taken from .
ifrst two components.
In this section we present an algorithm, based on statistical techniques and simulation, that allows us to estimate the robustness of a system s with respect to a DisTL formula . This algorithm consists in three basic steps: (i) A randomised procedure, based on simulation, that allows us to estimate the evolution time are used to estimate the distribution ds sequence of system s, assuming an initial data state ds: Starting from ds we sample sequences of data states d0 , . . . , d, for = 1, . . . , ; then all the data states collected at (ii) A mechanism to estimate the Wasserstein distance between two (unknown) distributions and on (, ℬ), similar to the one presented in [25]: To estimate W(m use independent samples {d11, . . . , d1 } taken from and ℓ independent samples ) we )(, (iii) A procedure that computes the robustness by inspecting the syntax of and by using the
The proposed approach has been implemented in Java, as part of Stark, and is available at
https://github.com/quasylab/jspear/tree/Tony. We omit the presentation of the first two steps (that
have already been discussed at length in [
The following theorem guarantees that when goes to infinite, the robustness computed by function Sat converges, almost surely, to the exact value.
Theorem 3. For any formula , system s, data state ds, time step , and integer ℓ > 0 lim Sat(ds, , , ℓ, ↦→∞ ) = J Kds , .
Proof. The proof follows by induction on the structure of the formula , using Theorem 2 to deal with the base cases of = target( ) and = brink( ).
Example 3. The procedure outlined above can be used for the evaluation of the requirements on the vehicle scenario presented in Example 2. Let be the evolution sequence of the system obtained from the following initial parameters: p_dist = 10000; p_speed = 25.0; MAX_SPEED = 40.0; A = 0.25; B = 2.0; TIMER = 1.0. In Figure 3a we report the evaluations, in and time step 0, of various instances of the formula 1. We consider a diferent instance for each 1 ∈ [250, 280], while we fix the other parameters: 2 = 350; = 100 and ℓ = 10. For each instance, we consider three variations, according to the threshold of the atomic formula: ∈ {0.1, 0.3, 0.5}.
Finally, we remark that J 2K, = 0.0 for all ∈ [0, 350], as shown in Figure 3b. In terms of robustness semantics, an evaluation to 0.0 is usually considered as non-informative, as it gives us no information on how much the behaviour of the system can be modified in order to validate (or invalidate) the considered property. However, in this specific case, 0.0 is the best value that we can obtain. In fact, the formula 2 contains a strict requirement on the speed, which is required to be exactly 0.0. Hence, J 2K, = 0.0 means that this requirement is actually met and, at the same time, even the tiniest modification in the behaviour might cause the formula to be invalidated.
(a) Evaluations of 1.
(b) Evaluations of 2.
Diferently from the other probabilistic temporal logics usually considered in the literature, DisTL can be used to express the properties of the distributions expressing the transient and expected behaviour of the system. Up to our knowledge, [26] is the only other paper proposing to substitute probabilistic guarantees on the temporal properties with a richer description of the probabilistic events. In detail, [26] introduces ProbSTL, a stochastic variant of STL tailored to the incremental runtime verification of safe behaviour of robotic systems under uncertainties, based on a predictive stream reasoning tool: their stochastic signal is given by the prediction on the possible future trajectories of a system, taking uncertainties into account. Yet, ProbSTL specifications are tested only on the current trajectory of the system. This is the main diference with our work, since our logic has been built to express the overall uncertain behaviour of the system. This disparity is also a consequence of the diferent application context: of-line verification for us, runtime verification in [ 26]. However, as future work, we plan to develop a predictive model for the runtime monitoring of DisTL specifications. In particular, inspired by [27, 28] where deep neural networks are used as reachability predictors for predictive monitoring, we intend to integrate our work with learning techniques, to favour the computation and evaluation of the predictions.
In Markov processes as transformers of distributions [29, 30], state-to-state transition probabilities are interpreted as a single distribution over the state space. We remark that the state space in [29, 30] is finite and discrete, whereas our evolution sequences are defined in the continuous setting, which means that we are not introducing any limiting assumption on the behaviour of the environment. Moreover, the temporal logics used to model check properties of transformers of distributions, respectively iLTL in [29] and the almost acyclic Büchi automata in [30], have a boolean semantics, and are thus not comparable to DisTL, in which formulae are interpreted in terms of robustness.
A statistical model checking algorithm for PCTL specifications over Markov chains has been proposed in [31], using stratified sampling. This allows for the generation of negatively correlated samples, thus reducing the number of samples needed to obtain confident results at the price of restricting the form of the PCTL formulae to be checked. We plan to study the use of stratified sampling in our model checking algorithm.
We also plan to investigate the application of our framework to the analysis of biological systems. Some quantitative extensions of temporal logics have already been proposed in that setting (e.g. [32, 33, 34]) to capture the notion of robustness from [35] or similar proposals [36]. It would be interesting to see whether the use of DisTL and evolution sequences can lead to new results in this setting.
This work has been partially supported by the project Programs in the wild: uncertainties, adaptability and verification (ULTRON) of the Icelandic Research Fund (grant No. 228376-051). This publication is part of the project NODES which has received funding from the MUR – M4C2 1.5 of PNRR with grant agreement no. ECS00000036. unknown environment, in: Proceedings of COORDINATION 2023, volume 13908 of Lecture Notes in Computer Science, 2023, pp. 115–132. doi:10.1007/978-3-031-35361-1_6. [13] H. Hansson, B. Jonsson, A logic for reasoning about time and reliability, Formal Asp.
Comput. 6 (1994) 512–535. doi:10.1007/BF01211866. [14] A. Aziz, K. Sanwal, V. Singhal, R. K. Brayton, Model-checking continous-time Markov chains, ACM Trans. Comput. Log. 1 (2000) 162–170. doi:10.1145/343369.343402. [15] A. Aziz, K. Sanwal, V. Singhal, R. K. Brayton, Verifying continuous time Markov chains, in: Proceedings of CAV ’96, volume 1102 of Lecture Notes in Computer Science, 1996, pp. 269–276. doi:10.1007/3-540-61474-5_75. [16] A. Pnueli, The temporal logic of programs, in: Proceedings of FOCS 1977, IEEE Computer
Society, 1977, pp. 46–57. doi:10.1109/SFCS.1977.32. [17] M. Tiger, F. Heintz, Stream reasoning using temporal logic and predictive probabilistic state models, in: Proceedings of TIME 2016, 2016, pp. 196–205. doi:10.1109/TIME.2016.28. [18] D. Sadigh, A. Kapoor, Safe control under uncertainty with probabilistic signal temporal logic, in: Proceedings of Robotics: Science and Systems XII 2016, 2016. doi:10.15607/ RSS.2016.XII.017. [19] R. Koymans, Specifying real-time properties with metric temporal logic, Real Time Syst. 2 (1990) 255–299. doi:10.1007/BF01995674. [20] O. Maler, D. Nickovic, Monitoring temporal properties of continuous signals, in: Proceedings of FORMATS and FTRTFT 2004, volume 3253 of Lecture Notes in Computer Science, 2004, pp. 152–166. doi:10.1007/978-3-540-30206-3_12. [21] L. N. Vaserstein, Markovian processes on countable space product describing large systems of automata., Probl. Peredachi Inf. 5 (1969) 64–72. [22] V. I. Bogachev, Measure Theory, number v. 1 in Measure Theory, Springer-Verlag,
Berlin/Heidelberg, 2007. doi:10.1007/978-3-540-34514-5. [23] O. P. Faugeras, L. Rüschendorf, Risk excess measures induced by hemi-metrics, Probability,
Uncertainty and Quantitative Risk 3:6 (2018). doi:10.1186/s41546-018-0032-0. [24] A. Donzé, O. Maler, Robust satisfaction of temporal logic over real-valued signals, in: Proceedings of FORMATS 2010, volume 6246 of Lecture Notes in Computer Science, 2010, pp. 92–106. doi:10.1007/978-3-642-15297-9_9. [25] D. Thorsley, E. Klavins, Approximating stochastic biochemical processes with Wasserstein pseudometrics, IET Syst. Biol. 4 (2010) 193–211. doi:10.1049/iet-syb.2009.0039. [26] M. Tiger, F. Heintz, Incremental reasoning in probabilistic signal temporal logic, Int. J.
Approx. Reason. 119 (2020) 325–352. doi:10.1016/j.ijar.2020.01.009. [27] D. Phan, N. Paoletti, T. Zhang, R. Grosu, S. A. Smolka, S. D. Stoller, Neural state classification for hybrid systems, in: Proceedings of ATVA 2018, volume 11138 of Lecture Notes in Computer Science, 2018, pp. 422–440. doi:10.1007/978-3-030-01090-4_25. [28] L. Bortolussi, F. Cairoli, N. Paoletti, S. A. Smolka, S. D. Stoller, Neural predictive monitoring, in: Proceedings of RV 2019, volume 11757 of Lecture Notes in Computer Science, 2019, pp. 129–147. doi:10.1007/978-3-030-32079-9\_8. [29] Y. Kwon, G. Agha, Linear inequality LTL (iltl): A model checker for discrete time markov chains, in: Proceedings of ICFEM 2004, volume 3308 of Lecture Notes in Computer Science, 2004, pp. 194–208. doi:10.1007/978-3-540-30482-1_21. [30] V. A. Korthikanti, M. Viswanathan, G. Agha, Y. Kwon, Reasoning about mdps as transformers of probability distributions, in: Proceedings of QEST 2010, IEEE Computer Society, 2010, pp. 199–208. doi:10.1109/QEST.2010.35. [31] Y. Wang, N. Roohi, M. West, M. Viswanathan, G. E. Dullerud, Statistical verification of PCTL using antithetic and stratified samples, Formal Methods Syst. Des. 54 (2019) 145–163. doi:10.1007/s10703-019-00339-8. [32] F. Fages, A. Rizk, On temporal logic constraint solving for analyzing numerical data time series, Theor. Comput. Sci. 408 (2008) 55–65. doi:10.1016/j.tcs.2008.07.004. [33] A. Rizk, G. Batt, F. Fages, S. Soliman, A general computational method for robustness analysis with applications to synthetic gene networks, Bioinform. 25 (2009). doi:10.1093/ bioinformatics/btp200. [34] A. Rizk, G. Batt, F. Fages, S. Soliman, Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures, Theor. Comput. Sci. 412 (2011) 2827–2839. doi:10.1016/j.tcs.2010.05.008. [35] H. Kitano, Towards a theory of biological robustness, Molecular Systems Biology 3 (2007) 137. doi:https://doi.org/10.1038/msb4100179. arXiv:https://www.embopress.org/doi/pdf/10.1038/msb4100179. [36] L. Nasti, R. Gori, P. Milazzo, Formalizing a notion of concentration robustness for biochemical networks, in: Proceedings of STAF 2018, volume 11176 of Lecture Notes in Computer Science, 2018, pp. 81–97. doi:10.1007/978-3-030-04771-9_8.