Studying Emergent Behaviours in Morphogenesis Using Signal Spatio-Temporal Logic

Abstract

Pattern formation is an important spatio-temporal emergent behaviour in biology. Mathematical models of pattern formation in the stochastic setting are extremely challenging to execute and analyse. Here we propose a formal analysis of the emergent behaviour of stochastic reaction diffusion systems in terms of Signal Spatio-Temporal Logic, a recently proposed logic for reasoning on spatio-temporal systems. We present a formal analysis of the spatio-temporal dynamics of the Bicoid morphogen in Drosophila melanogaster, one of the most important proteins in the formation of the horizontal segmentation in the development of the fly embryo. We use a recently proposed framework for statistical model checking of stochastic systems with uncertainty on parameters to characterise the parametric dependence and robustness of the French Flag pattern, highlighting non-trivial correlations between the parameter values and the emergence of the patterning.

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

One of the most fascinating questions in biology is how regular patterns can emerge from biochemical processes acting at the cellular level, a process known as morphogenesis in developmental biology. Some evident examples of these patterns can be observed in the stripes of a zebra, the spots on a leopard, the filament structure of the cyanobacteria Anabaena or the square pattern of the sulfur bacteria T. rosea. Mathematical and computational methods hold enormous promise in the quest to unveil the underlying mechanisms of morphogenesis and reproducing, using computer-based simulations, the patterns observed in nature. Alan Turing, mostly known as the father of computer science, was also a pioneer in developing a first mathematical model [28] that provides the chemical basis of morphogenesis. This model, also referred as the Turing’s reaction-diffusion system, is able to reproduce the formation of some complex patterns in nature such as the stripes seen in the animal skin.

Formal analysis of how patterns arise from mathematical models is however challenging due to the high computational burden of spatio-temporal modelling, as well as the intrinsic difficulty of defining spatio-temporal patterns in a suitable language. Pattern recognition is generally considered as a branch of machine learning [6], where patterns are classified according statistical descriptors (or features) [21] or the structural relationship among them [25]. This approach, despite its success and popularity, lacks of a rigourous foundation to specify such patterns and to reason about them in a systematic way. On the other end, formal methods provide logic-based languages [2, 10, 17, 18] with a well-defined syntax and semantics to specify in a precise and concise way emergent behaviours and the necessary techniques to automatically detect them.

Related Work. In the last year, two novel spatio-temporal logics, SpaTeL [18] and SSTL [10, 24] have made their appearance almost at the same time in the realm of formal methods to specify the emergence of spatio-temporal patterns.

The Spatial-Temporal Logic (SpaTeL) in [18] is the unification of Signal Temporal Logic [23] (STL) and Tree-Spatial-Superposition-Logic (TSSL) introduced in [2] to classify and detect spatial patterns. TSSL reasons over quad trees, spatial data structures that are constructed by recursively partitioning the space into uniform quadrants. TSSL is derived from Linear Spatial-Superposition-Logic (LSSL) [17], where the notion of superposition provides a way to describe statistically the distribution of discrete states in a particular partition of the space and the spatial operators correspond to zooming in and out of particular areas. In [17] the authors show also that by nesting these operators they are able to specify self-similar and fractal-like structures that generally characterize the patterns emerging in nature. SpaTeL is equipped with a qualitative (yes/no answer) and a quantitative semantics that provide a measure or robustness of how much the property is satisfied or violated. In [18] this measure of robustness is used as a fitness function to guide the parameter synthesis process for a deterministic reaction diffusion system using particle swarm optimisation (PSO) algorithms. However, the authors do not consider stochastic reaction-diffusion systems and PSO techniques generally do not provide any guarantee for reaching the global optimum. Hence, in this paper we will adopt a method with proved convergence guarantees, introduced previously in [3, 4] for the system design of stochastic processes using the robustness of temporal properties.

The Signal Spatio-Temporal Logic (SSTL) [10, 24] is the extension of STL [23] with three spatial modalities, somewhere, everywhere and surround, which can be nested arbitrarily with the original STL temporal operator. In [10, 24], the authors provide a qualitative and quantitative semantics of SSTL and efficient monitoring algorithms for both semantics. A more detailed description of SSTL is provided in Sect. 3. While in this paper we adopt SSTL to specify spatio-temporal patterns, the overall method for robust parameter synthesis for stochastic reaction diffusion systems presented here can be performed also using SpaTeL.

Contribution. In this work, we combine formal methods with statistical machine learning by presenting a novel analysis of a stochastic model of the spatio-temporal behaviour of the Bicoid protein in the Drosophila’s Embryo. The spatial gradient of this molecule has been shown to be at the basis of the subdivision of the embryo along its main axis, as specific concentration thresholds in its gradient are detected by cells and lead to the expression of distinct set of target genes.

The main technical contribution of the paper is the combination of SSTL within the statistical machine learning framework of [4, 7–9], in order to efficiently perform parameter space exploration and system design of spatio-temporal properties.

From a system biology perspective, instead, we present a detailed spatio-temporal analysis of the French Flag pattern on the gradient of the Bicoid protein. This analysis permits novel insights as to how the various model parameters interact to give rise to the patterning behaviour.

Paper Structure. The rest of the paper is organised as follows. In Sect. 2 we discuss the spatial pattern formation in the Drosophila embryos. In Sect. 3 we first recall the syntax and semantics of SSTL and then use it to specify the French Flag Property. The smoothed model checking and the parameter estimation is presented in Sect. 4. In Sect. 5, we present the results and we conclude with final remarks and directions for future work in Sect. 6.

2 Spatial Pattern Formation and the French Flag Model

In this section, we describe a model of segmentation in Drosophila melanogaster and the spatio temporal pattern characterising it, known as the French Flag model.

2.1 Pattern Formation and Reaction-Diffusion Systems

Patterning is a ubiquitous feature of biological organisms, and the presence of regular geometric motifs on many organisms has long fascinated scientists. Pattern formation is also the subject of one of the earliest, and most influential, computational systems biology works, Alan Turing’s pioneering work on morphogenesis [28]. Turing’s insight was that biological patterns can be viewed as emergent behaviour (in modern terminology) arising from local interactions of microscopic agents. More precisely, Turing considered spatially distributed systems whose local concentration vector $\mathbf {u}$ obeys a reaction-diffusion partial differential equation (PDE)

$$\begin{aligned} \frac{\partial \mathbf {u}}{\partial t}=D\nabla ^2\mathbf {u}+f(\mathbf {u}). \end{aligned}$$

(2.1)

Equation (2.1) defines the time evolution of the local concentration $\mathbf {u}$ as the sum of two terms: a dispersal or diffusion term $D\nabla ^2\mathbf {u}$, which globally drives the system towards a uniform equilibrium, and a reaction term $f(\mathbf {u})$, which accounts for local interactions of the chemicals. Turing then proved that, under certain conditions on the reaction/diffusion parameters, these two counteracting processes could give rise to regular patterns of concentration, providing a plausible mechanistic model of biological pattern formation.

Turing’s ideas have been empirically demonstrated in many areas of biochemistry (see [22] for a recent review), and are still influential in particular in the field of developmental biology (see e.g. [16] for a recent paper building on these ideas). The crucial idea in the application of reaction-diffusion systems to development is that these mechanisms would underpin the local concentration patterns of regulatory proteins, which would instruct different genetic programs to be executed at different spatial locations. These special regulatory proteins are called morphogens in developmental biology, as they are believed to be responsible for the establishment of the shape of an organism in higher organisms. One of the most widely studied models of morphogenesis is the establishment of spatial patterning (stripes) along the body of the fruit fly Drosophila melanogaster. Several morphogens are known in Drosophila; mostly, these are maternal proteins that are produced in a localised area of the embryo (in correspondence to a maternal deposit of messenger RNA), and then establish a concentration gradient during development, effectively providing cells within an embryo with a spatial reference. An important morphogen is the protein Bicoid, which is the central object of study in this paper and is described in detail in the next subsection.

Before closing this whirlwind review of developmental biology, it is worth remarking on a fundamental shift of perspective that has happened since Turing’s pioneering work, the realisation of the importance of stochasticity in biology. Numerous lines of evidence indicate that biology at the single cell level is intrinsically stochastic. Stochasticity cannot be ignored when modelling early embryogenesis, when only a handful of cells are present. Morphogenetic reaction-diffusion models can therefore be modified to account for the intrinsic discreteness of biology at the microscopic level. The natural analogue, systems of agents moving in continuous space, is however prohibitively expensive computationally; an approach that is more amenable to analysis is to discretise space into a number of cells (voxels) which are assumed to be spatially homogenous, and to replace spatial diffusion with transitions between different cells. Morphogenetic systems, and in particular the Bicoid system, have already been analysed from a simulation perspective in [31] and from a statistical perspective in [12]. In this paper, we present a first analysis of this system from the point of view of (spatio) temporal logic, to analyse directly the system’s behaviour at the level of the emergent properties of the trajectories.

2.2 The Bicoid Gradient

The Bicoid (Bcd) molecule was the first protein to be identified among the morphogens. In the Drosophila embryos, the Bcd protein is distributed along the Anterior-Posterior axis (A-P axis). The Bcd mRNA is translated at the anterior pole of the embryo, and the synthesised protein spreads through the A-P axis by diffusion accompanied by decay.

Fig. 1.

A schematisation of the Drosophila embryo volume. The volume is divided in 101 cubic subvolumes, , with side $l=5\,\mu m$.

We will describe the dynamics of the Bcd protein by a stochastic reaction-diffusion system, as reported in [31]. Given a certain volume where the Bcd protein is distributed, we can divide it into a series of subvolumes or voxels that are small enough to be regarded as well mixed. Then, we can consider the decay reaction as a transition that happens inside the subvolumes and the diffusion as exchange of molecules between neighbouring voxels. In particular, we consider 101 homogeneous cubic subvolumes with side $l=5\,\mu m$ that comprise the entire volume as in Fig. 1. The length of the side l and the number of subvolumes were chosen in light of those of actual Drosophila embryos, which are $500\,\mu m$ long. The first subvolume ($j = 0$), corresponds to the anterior pole of the embryo and it is the only subvolume where the Bcd protein is synthesised.

We can describe the set $\mathcal {R}$ of reactions governing the stochastic dynamics of Bcd as:

where $B_{j}$ is a Bcd protein in the jth subvolume.

The state vector of the system is then $\mathbf x _{B} = (x_{B_{0}},...,x_{B_{100}})$ where $x_{B_{j}}$ is the number of Bcd molecules in the jth subvolume. From the set $\mathcal {R}$ we can derive the infinitesimal generator matrix of the CTMC that formally represents the dynamics of the system. The CTMC can then be simulated with a standard algorithm, like SSA or tau-leaping.

Note that, from the set of reactions $\mathcal {R}$, we can easily revert the discretisation process and obtain a semantics in terms of Reaction-Diffusion Rate Equation (RDRE). This is obtained by converting variables into concentrations, taking the length of voxels to zero, and interpreting each rate as a flow, both in the degradation and in the diffusion reactions. In this way, we can define the system

$$\begin{aligned} \frac{\partial u}{\partial t}=D\frac{\partial ^{2} u}{\partial y} - w u, \end{aligned}$$

(2.2)

where u(y, t) is the concentration of Bcd at time t in position y, measured in $\mu m$, $y \in [0, 500]$, giving the boundary conditions $\frac{\partial u}{\partial y} \big |_{y=0}=- \frac{J}{\varDelta }$ and $\frac{\partial u}{\partial y} \big |_{y=500}=0$, where $\varDelta = l^{3}$.

2.3 Segmentation and the French Flag Model

The spatial distribution of the Bicoid protein has a crucial role in the formation of the horizontal segmentation in the development of the Drosophila’s embryo. One of the most important interpretations of this distribution is given by the French Flag model [29], and more generally by the theory of gap genes [19, 30]. The body of the fruit fly Drosophila melanogaster, as in most arthropods, exhibits a particular type of spatial patterning called segmentation, whereby the main body is composed of several segments. Gap genes were discovered and named following mutagenetic experiments, whereby biologists observed that deletion of certain genes resulted in the omission of a segment in the fly’s body, as if the mutant organism had a gap. This observation implies that gap genes must be expressed in a precisely spatially co-ordinated manner, i.e., the biochemistry of the fruit fly must possess a way of measuring distances.

The French Flag model is a simplified model of gap gene regulation in early embryogenesis involving only four genes, the Bicoid morphogen protein and three target genes. The underlying assumption is that the spatial distribution of Bicoid protein, which as we have seen tends to decrease along the A-P axis (see Fig. 2), provides the ruler with which the Drosophila embryo measures distances. Gap genes are activated in a concentration dependent manner by Bicoid, so that a set of genes are activated at the high concentrations near the anterior part of the embryo (the blue in the French Flag), a different set of genes is activated in the central part (the white) and a third set is activated a low concentrations near the posterior end (red). This model has survived with some modifications [20] until this day, its beauty providing a paradigm for pattern development in many areas of biology. From our point of view, this model is particularly interesting because it refocuses attention from local intensive quantities (local concentrations) towards the importance of a global emergent property of the system (the establishment of a gradient), which is ideally suited for reasoning upon in terms of spatio-temporal logics. We will see in the next section this how to describe the French Flag pattern using a spatio-temporal logic.

3 Formula Specification of Spatio-Temporal Behaviour

In this section, we describe Signal Spatio-Temporal Logic (SSTL) which will then be used to specify the spatio-temporal behaviour of the French Flag pattern.

3.1 Signal Spatio-Temporal Logic

The Signal Spatio-Temporal Logic (SSTL) [10, 24] is a linear time logic suitable to specify spatio-temporal behaviours of traces generated from simulations. It is an extension of Signal Temporal Logic (STL) [23] with two spatial modalities.

The space is described as a weighted graph $G = ( L , E, w)$ where L is a set of locations, E is a set of edges and $w: E \rightarrow \mathbb {R}_{\ge 0}$ is the function that returns the cost/weight of each edge, typically encoding the distance between two nearby locations.

The syntax of SSTL is given by

where the STL operators are the atomic proposition $\mu$, the standard boolean connectives conjunction and negation and the bounded until operator $\mathcal {U}_{I}$, with I a dense-real interval. The new spatial operators are the somewhere operator, , and the bounded surround operator $\mathcal {S}_{[ w_{1}, w_{2}]}$, where $[w_{1},w_{2}]$ is a closed real interval with $w_{1} < w_{2}$. The spatial somewhere operator requires $\varphi$ to hold in a location reachable from the current one with a total cost greater than or equal to $w_{1}$ and less than or equal to $w_{2}$. The surround formula $\varphi _{1} \, \mathcal {S}_{[ w_{1}, w_{2}]} \varphi _{2}$, instead, is true in a location $\ell$ when $\ell$ belongs to a subset of locations A, a region, satisfying $\varphi _1$, such that its external boundary $B^{+}(A)$ (i.e., all the nearest neighbours of locations in A) contains only locations satisfying $\varphi _2$. Furthermore, locations in $B^{+}(A)$ must be reached from $\ell$ by a shortest path of cost between $w_{1}$ and $w_2$, i.e. they have to be at distance between $w_{1}$ and $w_{2}$ from $\ell$. There are also three derivable operators: the eventually operator $\mathcal {F}_{I} \, \varphi := \texttt {true}\, \mathcal {U}_{I} \, \varphi$, the always operator $\mathcal {G}_{I} \, \varphi := \lnot \, \mathcal {F}_{I} \, \lnot \, \varphi$ and the everywhere operator that requires $\varphi$ to hold in all the locations reachable from the current one with a total cost between $w_{1}$ and $w_{2}$.

SSTL is interpreted on spatio-temporal traces $\mathbf x : \mathbb {T} \times L \rightarrow \mathbb {R}^{n}$, where $\mathbb {T}$ is the time domain, usually a real interval [0, T], with $T>0$; we can write the trace as ${ \mathbf x (t, \ell )}=(x_{1}(t, \ell ), \cdots , x_{n}(t, \ell ))$, where each $x_{i}: \mathbb {T} \times L \rightarrow \mathbb {R}$, for $i= 1,...,n$, is the projection on the $i^{th}$ coordinate/variable.

Similarly to STL, SSTL has two semantics, the classical boolean semantics and a quantitative semantics.

The boolean semantics returns true or false depending on whether the trace satisfies the SSTL property, i.e. $(\mathbf x , t, \ell ) \models \varphi$ is true if and only if the trace $\mathbf x (t,\ell )$ satisfies $\varphi$. By convention, the whole trace satisfies a property in location $\ell$ iff it satisfies the property at time zero, i.e. $(\mathbf x , \ell ) \models \varphi \Leftrightarrow (\mathbf x ,0, \ell ) \models \varphi$.

The quantitative semantics, instead, returns a real value $\rho (\varphi , \mathbf x ,t, \ell )$ that quantifies the level of satisfaction of the formula by the trajectory $\mathbf x$ at time t in location $\ell$. The absolute value $|\rho (\varphi , \mathbf x ,t,\ell )|$ can be interpreted as measure of the robustness of the satisfaction or dissatisfaction. Furthermore, the sign of $\rho (\varphi , \mathbf x ,t,\ell )$ is related to the truth of the formula: if $\rho (\varphi , \mathbf x ,t,\ell ) > 0$, then $(\mathbf x ,t, \ell ) \models \varphi$, and similarly if $\rho (\varphi , \mathbf x ,t,\ell ) < 0$, then $(\mathbf x ,t, \ell ) \not \models \varphi$. The definition of this quantitative measure $\rho$ is based on [13, 14], and it is a reformulation of the robustness degree of [15]. In accordance with the boolean semantics, the quantitative value of the whole trace in location $\ell$ is given by its value at time zero, i.e. $\rho (\mathbf x ,\ell )= \rho (\mathbf x , 0, \ell )$.

SSTL is equipped with efficient monitoring algorithms for both the boolean and the quantitative semantics, whose description, together with a formalisation of the semantics, can be found in [10, 24].

3.2 The French Flag Property

To describe the French Flag pattern we have first to define the trajectories that we want to characterise and its related graph.

Let consider a trace (a simulation) $( \mathbf x _{B}(t) )_{t \in [0, T]}=(x_{B_{0}}(t), ..., x_{B_{100}}$ $(t))_{t \in [0, T]}$ of the Bicoid model described in the previous section, where [0, T] is the time domain, with $T>0$. We can transform the temporal trace in a spatio-temporal trajectory defining $x_{B}: L \times [0,T]\rightarrow \mathbb {R}$ s.t. $x_{B} (V_{i}, t):=x_{B_{i}}(t)$, where $L=\{ V_{0}, ..., V_{100}\}$ is the set of locations. The graph $G=(L,E,w)$ of the system is a one-dimensional graph where each $V_{i}$ is connected only to $V_{i-1}$ and $V_{i+1}$, with $w(V_{i},V_{i+1})=1$, i.e. all the edges have weight equal to 1. The weight between two arbitrary locations is given by the weight of the shortest path connecting them.

We can now use the logic to specify the French Flag model. As we described in Sect. 2, this pattern is used to represent the effect of a morphogen in the expression of different genes, i.e. to represent the correlation between the concentration of the morphogen and the activation or repression of other genes. In particular, the spatial distribution of the morphogen, at the steady state, is divided in three regions: a blue, a white and a red region, as shown in Fig. 2 (left), that activate different target genes.

We can describe this behaviour with the property

$$\begin{aligned} \psi _{flag} := \varphi _{blue} \wedge \varphi _{white} \wedge \varphi _{red} \end{aligned}$$

(3.3)

(3.4)

The verification of the formula is done in the location $V_{0}$. $(x, V_{0}) \models \psi _{flag}$ iff it satisfies each subformulae $\varphi _{blue},\varphi _{white}, \varphi _{red}$; $(x,V_{0}) \models \varphi _{blue}$ iff, in all the locations $V_{i}$ s.t. $w(V_{0},V_{i}) \le w_{blue}$, the number of Bicoid molecules is higher than $K_{blue} - h_{bw}$, i.e. $x_{B} > K_{blue} - h_{bw}$. In a similar way we can describe $\varphi _{white}$ and $\varphi _{red}$. The meaning of the property is that the spatial distribution of the Bicoid protein is divided in three regions, the blue, where the $x_{B} > K_{blue} - h_{bw}$, the white, where $K_{blue} + h_{bw} > x_{B} > K_{white} - h_{wr}$, and the red, where $x_{B} < K_{white} + h_{wr}$. Note that $h_{bw}$ and $h_{wr}$ parameters have the role to relax the thresholds that define different regions, to properly deal with noise in Bcd expression, we will discuss this point more in detail in the Sect. 5.1.

At steady state, the concentration of the Bicoid protein is exponentially distributed along the anterior-posterior (A-P) axis, with higher concentrations towards the anterior. We can identify the insurgence time of this pattern, and if it remains stable, combining the spatial property with temporal operators as follows:

$$\begin{aligned} \begin{array}{lcl} \psi _{stable flag} &{} := &{} \mathcal {F}_{[T_{flag}, T_{flag} + \delta ]} (\mathcal {G}_{[0, T_{end}]} \psi _{flag})\\ \end{array} \end{aligned}$$

(3.5)

$\psi _{stable flag}$ means that eventually, in a time between $T_{flag}$ and $T_{flag} + \delta$, the property $\psi _{flag}$ remains true for at least $T_{end}$ time units.

4 Methodologies

The main objective of this work is to study the effects of the Bicoid parameters on the satisfaction of the French Flag property. Exhaustive parameter exploration is particularly expensive for the model in question, due to the high cost of stochastic simulation. In this section, we briefly introduce the methodologies that we use to perform parameter synthesis and model checking in presence of parametric uncertainty.

4.1 Smoothed Model Checking

The Smoothed Model Checking algorithm [7] relies on the characterisation of the satisfaction probability of a formula $\varphi$ as a function of the parameters. Given a CTMC $\mathcal {M}_{\theta }$, whose transition rates depend on a set of parameters $\theta$, the satisfaction function of $\varphi$ is defined as follows:

$$\begin{aligned} f(\theta ) \equiv p(\varphi =\texttt {true}\vert \mathcal {M}_\theta ) \end{aligned}$$

It has been proven in [7] that, if the transition rates of $\mathcal {M}_{\theta }$ depends smoothly on the parameters $\theta$ and polynomially on the state of the system, then the satisfaction function of $\varphi$ is a smooth function of the parameters.

The smoothed model checking approach leverages of the smoothness of the satisfaction function and transfers information across nearby parameter values. More specifically, we place a Gaussian Process (GP) prior over the space of possible functions, and we evaluate the satisfaction function for a set of parameter values. We then calculate the GP posterior under the light of these observations, which constitutes analytical approximation to the satisfaction function. This implies that we can estimate the satisfaction probability at any point in the parameter space with no additional cost.

The premise is that fewer samples are required to achieve a given level of accuracy. In the experiments of [7], it has been possible to accurately approximate the satisfaction function over a wide range of parameters using less than 10 % of the simulation runs required to obtain the same result with exhaustive parameter exploration. This resulted in a decrease of the total analysis time nearly by 90 %.

4.2 Robust Parameter Synthesis

The problem of robust parameter synthesis constitutes of identifying the model parameters that maximise the robustness of some desired property. According to the quantitative semantics of SSTL, the robustness value $\rho (\varphi , \mathbf x ,t, \ell )$ expresses the level of satisfaction of $\varphi$ by a trajectory $\mathbf x$ at time t in location $\ell$. Since trajectories are random for a stochastic system, we designate the robustness of $\varphi$ for a CTMC as a random variable $R_{\varphi }$. We are therefore interested in maximising the expected quantitative score:

$$\begin{aligned} E[R_{\varphi }] = \int \rho (\varphi , \mathbf x ,t,\ell ) p(\mathbf x ) d\mathbf x \end{aligned}$$

(4.6)

where $p(\mathbf x )$ is the probability density of trajectory $\mathbf x$. For a specified time t and location $\ell$, the expectation $E[R_{\varphi }]$ constitutes an objective function, for which we can obtain noisy estimates by generating samples from the trajectory space via stochastic simulation.

Since evaluating the expected robustness is computationally expensive, we employ the Gaussian process optimisation algorithm described in [9]. In short, the objective function is approximated by a Gaussian Process (GP). The algorithm is initialised with a random grid of points, for each of which $E[R_{\varphi }]$ is approximated via statistical means. Using these points as a training set, a GP is used to make predictions regarding the $E[R_{\varphi }]$ value at different parts of the search space, without exhaustive exploration of the parameter space. We calculate the GP posterior for a set of test points; that involves calculating an estimate of the expected robustness and its associated variance. The GP optimisation algorithm dictates that the point that maximises the an upper quantile of the GP posterior is added to the training set, after being evaluated for its associated robustness via SMC. A high value for the upper quantile at any point in the parameter space indicates the possibility of an undiscovered maximum nearby. This feature allows us to direct the search towards areas of the parameter space that appear to be more promising. This process is repeated for a number of iterations, and the training set is progressively updated with new potential maxima. For a smooth objective function, the algorithm is proved to converge to the global optimum in [27].

5 Results

In this section, we perform a series of experiments to explore the sensitivity and robustness of the French Flag property w.r.t. changes in the rates of production J and degradation w, and the diffusion rate parameter D. The size of the cubic subvolumes is known, that is $l=5 \mu m$, as it is one of the main modelling assumptions.

5.1 Experimental Data

Following [26, 31], we chose as parameters of the $\psi _{stableflag}$ property (3.5), specified in Sect. 3.2, $T_{flag}= 3950$, $\delta = 10$, $T_{end} = 1000$, $w_{blue} = 35.5$, $w_{while} = 67.5$ and $w_{max}=101$. The $w_{blue}$ and $w_{while}$ parameters mean that the blue area involves the subvolumes between $V_0$ and $V_{35}$, the white area extends from volume $V_{36}$ to $V_{67}$, and finally the red one from $V_{68}$ to $V_{100}$; the time is in terms of seconds.

In order to fix the thresholds parameters $K_{blue}$, $K_{white}$ and $h_{bw}$,$h_{wr}$ we use the Bicoid fluorescence concentration at cycle 13 (where the gradient is considered to be in the steady state) downloaded from the FlyEx database [1]. The choice of the data follows the analysis doing in [31]. To the best of our knowledge, all the quantifications of the Bicoid protein in the Drosophila embryo refers to the measurements of fluorescence concentrations, rather than direct observations of the Bicoid molecular population. From [31], we define the fluorescence concentration $I = m \times x_{B}$, where m is a scaling factor that denotes the fluorescence-to-molecule ratio. Our approach is to rescale the thresholds reported in terms of fluorescence concentrations with the m factor.

The data has been given originally in the form of two-dimensional coordinates paired, the A-P and D-V coordinate, from the central $10\,\%$ strip. As in [31], we choose the embryos where the variation inside each spatial subregions is low, in particular in these embryos the inverse of the spatial exponential coefficient varied by less that $1\,\%$. We have transformed the data so that we have a single concentration value for each of the 101 discretised locations. Figure 2 depicts the result. On the left-side figure, we see how the different locations lie within the areas prescribed by the French Flag property. Although the shape of the data is apparently negative exponential, there is a considerable amount of noise, which has to be taken into consideration in terms of the French Flag property. We therefore define the thresholds in the form regions, rather than strict values. On the right-side of Fig. 2, we see a magnified version of the figure, where only the white area is depicted. The majority of the concentrations recorded for volumes from $V_{36}$ to $V_{67}$ are between 60 and 2. In the same way, we can empirically derive zones of desired concentration levels for the blue and read areas. Therefore we have $K_{blue} = 45/m$, $h_{bw} = 15/m$, $K_{white} = 6/m$, and $h_{wr} = 4/m$.

Fig. 2.

Left: Fluorescence concentrations of the Bicoid protein for 17 embryos during the cycle 13. Right: The same concentrations in the area between locations 35 and 67, which define the white area in the French flag property.

5.2 Optimisation of Expected Robustness

We now explore how the model parameters (including the scaling factor m) can be tuned to increase the robustness of the French Flag pattern.

We applying the GP optimisation algorithm discussed in Sect. 4.2, for a four-dimensional space that involves the parameters: $w \in [0.001, 0.01]$, $J \in [10, 400]$, $D \in [1, 40]$, and $m \in [0.01, 1]$. The parameter ranges have been selected so that the resulting space is a superset of the explored space in [31]. Regarding the fluorescence-to-molecule ratio in particular, we note that the extremes considered in [31] have been 0.07 and 0.7.

For each evaluation of the expected robustness, the system has been simulated up to time $t = 4000$ s, which is when the steady-state is approached according to [31]. The robustness expectation has been approximated statistically using 12 simulation runs for each parameter set. The algorithm has been initialised by 80 evaluations of the objective function at random points; a number of 282 evaluations were performed at points selected by the optimisation process, until convergence was detected. Convergence has been determined when no significant improvement of the expected robustness has been observed for 200 iterations. An improvement is considered significant, if it is more than 1 % increase over the previously recorded maximum robustness.

In the end, a total of 362 function evaluations have been performed, which is arguably a small number of samples to explore a four-dimensional space. The execution times have been 85 min for the initial 80 evaluations, and 263 min for the actual optimisation process. Stochastic simulations have been performed in parallel using 12 threads. The experiments have been performed on an Intel^® Xeon^® CPU E5-2680 v3 2.50 GHz. The majority of the computational effort was spent in simulation, despite the fact that only 12 trajectories have been generated for each parameter set considered. Therefore the idea of reducing the number of samples by exploiting the smoothness of the objective function has been a sensible practice.

The values returned by the optimisation process have been: $w^{*} = 0.0038$, $J^{*} = 390$, $D^{*} = 32.5$, and $m^{*} = 0.048$. The robustness of the optimum returned has been 2.99, implying that the property is robustly satisfied for the given solution. In Fig. 3, we present a sample trajectory for the given parameter configuration, and the average of 40 random trajectories, along with the associated 99.8 % confidence bounds. The sample trajectory is plotted against the experimental data that were used to adjust the threshold parameters of the French Flag property. We see that the optimised model has a behaviour very similar to the one observed in real-world experiments. However, it appears that the simulation results are much less noisy, when compared to the actual observations. This finding is in agreement with the result of [31], where it was argued that the intrinsic noise as modelled by the stochastic dynamics of the master equation is not sufficient to explain the variability in the data, i.e. the noise in the fluorescence measurement as a crucial role that has to be taken into account.

Fig. 3.

Left: Sample trajectory for the parameter configuration that maximises the robustness of the French Flag property. Right: Average of 40 random trajectories; the dotted lines indicate the 99.8 % confidence interval.

5.3 Parameter Exploration with Smoothed Model Checking

In this section, we perform a more thorough exploration of the parameter space. Our objective is to discover dependencies among the parameters, considering the satisfaction probability of the French Flag property. On that respect, the fluorescence-to-molecule ratio m is not significant, as this will have an obvious effect on the thresholds for the property. We fix the fluorescence-to-molecule ratio m to 0.048, which is the optimal value reported by the optimisation algorithm in the previous section. The rest of the model parameters, $w \in [0.001, 0.01]$, $J \in [10, 400]$, and $D \in [1, 40]$, are explored via the smoothed model checking approach.

During the initialisation step of the algorithm, we have performed 216 evaluations of the satisfaction function of (3.3), for a regularly distributed set of values. As in the previous section, the satisfaction probability is approximated by statistical model checking using 12 simulation runs for each parameter configuration, where the system is simulated up to time $t = 4000$ s.

The duration of this initial statistical model checking process has been nearly 170 min, on an Intel^® Xeon^® CPU E5-2680 v3 2.50 GHz, using 12 threads in parallel. The hyperparameter optimisation that is required to tune the GP probit regression model subsequently required only 20 s, which is a trivial price to pay compared to the massive simulation cost. The final GP probit regression for a grid of 4096 points required only 1.2 s. Most importantly, it is only this last cost that we are required to pay to produce any further estimations of the satisfaction function.

Figure 4 depicts the satisfaction function for the French Flag property for parameters $\theta = \{w, J, D\}$, as this has been approximated by smoothed model checking. Each of the depicted subfigures shows the satisfaction probability as function of the production rate J and the diffusion parameter D, for a different value of the degradation rate w. Regarding the confidence of the estimated probabilities, we report that the 73.6 % of the values are associated with 95 % confidence intervals of width less than 0.2.

As a general remark, it appears that the manifestation of the gradient pattern, as this is captured by the French Flag property, is associated with a fine balance among the model parameters. There is a small area in the parameter space for which the property is satisfied with high probability. As we increase the decay parameter w however, we observe two behaviour regarding this area: its size is being increased, and its location is being shifted to the right. This implies that w is positively correlated with the production rate J. In other words, a particular ratio between protein production and decay is required for the formation of the particular pattern. At the same time, increasing the decay rate means that the formula may be satisfied for a wider range of the diffusion parameter.

It also appears that there is a negative correlation between the production rate J and the diffusion parameter D. This behaviour is present for the entire range of w examined, but it tends to become more obvious as w is increased. It is reasonable to conclude that a simultaneous increase of J and D would destroy the exponential shape of the Bicoid distribution across space.

Fig. 4.

Emulated satisfaction probability of the French Flag property as function of $\theta = \{w, J, D\}$. Each subfigure has the w parameter fixed.

6 Conclusions

We present a framework for the formal analysis under parametric uncertainty and the robust parameter synthesis of spatio-temporal properties emerging in a stochastic reaction-diffusion system. These properties are specified using the spatio-temporal logic SSTL. The framework combines statistical machine learning techniques based on Gaussian processes with the algorithm for monitoring SSTL properties.

As a case study, we analyse the occurrence of the French Flag pattern in the Bicoid gradient, during the development of Drosophila embryo. Analysing how this property depends on the parameters of the model is challenging due to the very high computational cost of simulating a spatio-temporal model, and has only been possible by adopting recent efficient verification techniques that employ machine learning methodologies [8]. Furthermore, the combination of these new techniques with SSTL permits exploring behaviours that are extremely difficult to express (and monitor) with standard temporal logics, where each individual location would need to be accounted.

The natural extension of this work is the analysis of more complicated models and properties, for example adding to this model the proteins of the target genes related with the spatial distribution of the Bicoid protein, enabling the study of the spatial dependency between proteins. To be independent from the spatial approximation, we plan also to consider different discretisation of the Drosophila’s volume. Another future work could be the consideration of a model rescale with a random factor that mimics the extrinsic noise due to the fluoresce measurements. We plan also to extend our previous result in mining temporal logic properties [5, 11] for the spatio-temporal case. Finally, we are considering an extension of the logic to continuous spaces and we would like to compare the expressiveness of SSTL with SpaTeL.