Pârvu Ovidiu, Gilbert David
Department of Computer Science, Brunel University, Kingston Lane, Uxbridge, UB8 3PH, London, UK.
BMC Syst Biol. 2014 Dec 2;8:124. doi: 10.1186/s12918-014-0124-0.
Computational models play an increasingly important role in systems biology for generating predictions and in synthetic biology as executable prototypes/designs. For real life (clinical) applications there is a need to scale up and build more complex spatio-temporal multiscale models; these could enable investigating how changes at small scales reflect at large scales and viceversa. Results generated by computational models can be applied to real life applications only if the models have been validated first. Traditional in silico model checking techniques only capture how non-dimensional properties (e.g. concentrations) evolve over time and are suitable for small scale systems (e.g. metabolic pathways). The validation of larger scale systems (e.g. multicellular populations) additionally requires capturing how spatial patterns and their properties change over time, which are not considered by traditional non-spatial approaches.
We developed and implemented a methodology for the automatic validation of computational models with respect to both their spatial and temporal properties. Stochastic biological systems are represented by abstract models which assume a linear structure of time and a pseudo-3D representation of space (2D space plus a density measure). Time series data generated by such models is provided as input to parameterised image processing modules which automatically detect and analyse spatial patterns (e.g. cell) and clusters of such patterns (e.g. cellular population). For capturing how spatial and numeric properties change over time the Probabilistic Bounded Linear Spatial Temporal Logic is introduced. Given a collection of time series data and a formal spatio-temporal specification the model checker Mudi ( http://mudi.modelchecking.org ) determines probabilistically if the formal specification holds for the computational model or not. Mudi is an approximate probabilistic model checking platform which enables users to choose between frequentist and Bayesian, estimate and statistical hypothesis testing based validation approaches. We illustrate the expressivity and efficiency of our approach based on two biological case studies namely phase variation patterning in bacterial colony growth and the chemotactic aggregation of cells.
The formal methodology implemented in Mudi enables the validation of computational models against spatio-temporal logic properties and is a precursor to the development and validation of more complex multidimensional and multiscale models.
计算模型在系统生物学中对于生成预测起着越来越重要的作用，在合成生物学中作为可执行的原型/设计。对于实际生活（临床）应用，需要扩大规模并构建更复杂的时空多尺度模型；这些模型能够研究小尺度变化如何在大尺度上反映，反之亦然。只有在模型首先经过验证的情况下，计算模型产生的结果才能应用于实际生活应用。传统的计算机模拟模型检查技术仅捕捉无量纲属性（如浓度）如何随时间演变，适用于小规模系统（如代谢途径）。对更大规模系统（如多细胞群体）的验证还需要捕捉空间模式及其属性如何随时间变化，而传统的非空间方法并未考虑这一点。
我们开发并实施了一种针对计算模型的空间和时间属性进行自动验证的方法。随机生物系统由抽象模型表示，该模型假设时间具有线性结构，空间采用伪三维表示（二维空间加上密度度量）。由此类模型生成的时间序列数据作为输入提供给参数化图像处理模块，该模块自动检测和分析空间模式（如细胞）以及此类模式的集群（如细胞群体）。为了捕捉空间和数值属性如何随时间变化，引入了概率有界线性空间时间逻辑。给定一组时间序列数据和一个形式化的时空规范，模型检查器Mudi（http://mudi.modelchecking.org）以概率方式确定形式化规范是否适用于计算模型。Mudi是一个近似概率模型检查平台，它使用户能够在频率主义和贝叶斯方法之间进行选择，基于估计和统计假设检验的验证方法。我们基于两个生物学案例研究，即细菌菌落生长中的相变模式和细胞的趋化聚集，说明了我们方法的表达能力和效率。
Mudi中实现的形式化方法能够针对时空逻辑属性对计算模型进行验证，并且是开发和验证更复杂的多维和多尺度模型的先驱。
