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

Abstract

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.

Fig 1. Multiscale spatio-temporal model checking workflow.

The first step (1) in the workflow is using biological observations and/or information from the literature to construct the multilevel computational model of the biological system considered. Next (2) the model is simulated to produce time series data in which spatial entities from multiple scales are automatically detected and analysed using a multiscale spatio-temporal analysis module. Then (3) the specification against which the model is verified is translated from natural language to a formal multiscale spatio-temporal language called PBLMSTL. Finally (4) using the model checker Mule the model is automatically verified relative to the given PBLMSTL specification considering the processed time series data representing the modelled system behaviour. If the model is declared incorrect relative to the given specification then it is updated and the steps (2) and (4) are repeated.

Fig 2. Initial state of the system.

Cell and A_extracellular are the spatial state variables representing the position of the cell, respectively distribution of nutrient A in the environment. A_intracellular and Energy represent the intracellular availability of nutrient A, respectively energy.

Fig 3. The state space of the system i.e. all possible states which can be reached from the initial state S₀.

Cell and A_extracellular are the spatial state variables representing the position of the cell, respectively distribution of nutrient A in the environment. A_intracellular and Energy represent the intracellular availability of nutrient A, respectively energy. The percentage associated with the arrows connecting each pair of states represents the probability of transitioning from one state to the other.

Fig 4. The multiscale architecture graph corresponding to the simple illustrative MSSpDES example.

Each vertex in the graph (e.g. (Environment, GrowthMedia)) corresponds to a subsystem (e.g. growth media) and its associated scale (e.g. environment). Directed edges between vertices (e.g. ((Environment, GrowthMedia), (Cellular, Microorganism))) indicate how one subsystem from a coarse-grained scale (e.g. (Environment, GrowthMedia)) can be decomposed in one or multiple subsystems from more fine-grained scales (e.g. (Cellular, Microorganism)).

Fig 5. The multiscale spatio-temporal analysis workflow.

An MSSpDES model of the system under consideration is constructed and simulated to generate time series data. This time series data is split up into subsets (1) such that each subset corresponds to a single subsystem and scale. The time series data subsets are passed to a uniscale spatio-temporal analysis module (2) which automatically detects, analyses and annotates spatial entities with their corresponding scale and subsystem. The results of the uniscale spatio-temporal analysis are then merged (3) such that spatial entities corresponding to the same time point are grouped together. If more simulations are required, a new time series dataset is generated, for which steps (1)–(3) are repeated.

Fig 6. Workflow for creating multiscale spatio-temporal model checking methodology instances.

The workflow comprises two levels, the upper generic (meta) level, and the lower specific (instance) level. The upper level comprises the multiscale spatio-temporal meta model checking methodology. Conversely the lower level consists of the specific collections of spatial entity types and measures employed to create multiscale spatio-temporal model checking methodology instances. For each considered pair (e.g. m) of spatial entity types and spatial measures collections a corresponding multiscale model checking methodology instance is created. The resulting methodology instances (e.g. m) can then be employed for various case studies (e.g. n) to decide if computational models (e.g. m,n) are correct relative to corresponding formal specifications (e.g. m,n) or not. Rounded rectangles and arrows having the same border/line colour correspond to the same collections of spatial entity types and spatial measures.

Fig 7. Implementation of workflow for generating multiscale spatio-temporal model checker instances according to user-defined spatial entity types and spatial measures.

Starting from the problem one tries to solve, an xml file is created describing the collections of spatial entity types and spatial measures of interest. These collections are then verified with respect to relevant constraints captured by an xsd file; see http://mule.modelchecking.org/standards for the latest version of the xsd file. If the xml file verification fails then the specification of the spatial entity types and measures needs to be updated accordingly. Otherwise the xml file is employed by a C++ source code generator/translator written in Python to generate the corresponding Mule source files based on a set of predefined templates. The source files are compiled to produce an executable version of the corresponding Mule instance. This instance can then be employed to verify corresponding computational models.

Fig 8. MA graph representing the multiscale organization of the rat cardiovascular system dynamics computational model.

Fig 9. MA graph representing the multiscale organization of the uterine contractions of labour computational model.

Fig 10. MA graph representing the multiscale organization of the Xenopus laevis cell cycle computational model.

Fig 11. MA graph representing the multiscale organization of the acute inflammation of the gut and lung computational model.

Fig 12. Average execution times (measured in seconds) corresponding to the verification of the rat cardiovascular system dynamics, the uterine contractions of labour, the Xenopus laevis cell cycle, and the acute inflammation of the gut and lung computational models.

Execution times were recorded for the computational model simulation, converting the output to csv format, generating MSTML subfiles for each considered time point, numeric state variable and spatial entity, merging the subfiles into a single MSTML file, and model checking.