A Novel Method to Verify Multilevel Computational Models of Biological Systems Using Multiscale Spatio-Temporal Meta Model Checking.

Insights gained from multilevel computational models of biological systems can be translated into real-life applications only if the model correctness has been verified first. One of the most frequently employed in silico techniques for computational model verification is model checking. Traditional model checking approaches only consider the evolution of numeric values, such as concentrations, over time and are appropriate for computational models of small scale systems (e.g. intracellular networks). However for gaining a systems level understanding of how biological organisms function it is essential to consider more complex large scale biological systems (e.g. organs). Verifying computational models of such systems requires capturing both how numeric values and properties of (emergent) spatial structures (e.g. area of multicellular population) change over time and across multiple levels of organization, which are not considered by existing model checking approaches. To address this limitation we have developed a novel approximate probabilistic multiscale spatio-temporal meta model checking methodology for verifying multilevel computational models relative to specifications describing the desired/expected system behaviour. The methodology is generic and supports computational models encoded using various high-level modelling formalisms because it is defined relative to time series data and not the models used to generate it. In addition, the methodology can be automatically adapted to case study specific types of spatial structures and properties using the spatio-temporal meta model checking concept. To automate the computational model verification process we have implemented the model checking approach in the software tool Mule (http://mule.modelchecking.org). Its applicability is illustrated against four systems biology computational models previously published in the literature encoding the rat cardiovascular system dynamics, the uterine contractions of labour, the Xenopus laevis cell cycle and the acute inflammation of the gut and lung. Our methodology and software will enable computational biologists to efficiently develop reliable multilevel computational models of biological systems.

Automatic validation of computational models using pseudo-3D spatio-temporal model checking.

BACKGROUND: 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. RESULTS: 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. CONCLUSIONS: 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.

Fractal analysis of ibuprofen effect on experimental dog peri-implantitis.

INTRODUCTION: The aim of this study was to assess the correlation between the fractal analysis of gingival changes and systemic nitro-oxidative stress in a short-term low-dose ibuprofen (IBU) treatment at experimental peri-implantitis (PI). MATERIALS AND METHODS: Six adult male mixed-breed dogs with PI were randomly treated for 2 weeks, 3 with IBU (5 mg/kg b.w.) and 3 with placebo. Clinical and radiological evaluation were performed. Gingival biopsies were assessed by light microscopy, transmission electron microscopy, and fractal analysis. Blood was collected to assay nitric oxide (NOx), total oxidative status (TOS), total antioxidant response (TAR), and oxidative stress index (OSI). RESULTS: Specific gingival ultrastructural alterations, bone loss, and systemic nitro-oxidative stress were evident in PI-placebo animals. IBU caused significant clinical, microscopic, fractal dimensions (P < 0.01), NOx, TOS, and OSI improvements. IBU caused no important bone and TAR changes. CONCLUSION: This study confirms that fractal analysis was a good method to assess the complex morphological changes and correlations with the nitro-oxidative stress in PI. Short-term low-dose IBU treatment consistently improved gingival status and reduced systemic nitro-oxidative stress.