Automatic validation of computational models using pseudo-3D spatio-temporal model checking | JoVE Visualize

Area of Science:

Systems Biology
Computational Biology
Synthetic Biology

Background:

Computational models are vital for systems and synthetic biology predictions and designs.
Scaling up models for clinical applications requires handling complexity, multiscale interactions, and spatio-temporal dynamics.
Traditional model checking methods are limited to non-dimensional, temporal properties, insufficient for large-scale spatial systems.

Purpose of the Study:

To develop and implement a methodology for the automatic validation of computational models.
To address the need for validating models that incorporate both spatial and temporal properties.
To enable the validation of complex, spatio-temporal, multiscale biological models.

Main Methods:

Representing stochastic biological systems using abstract models with linear time and pseudo-3D space.
Utilizing parameterized image processing modules to analyze spatial patterns and clusters from time-series data.
Introducing Probabilistic Bounded Linear Spatial Temporal Logic for analyzing spatio-temporal properties.
Employing the Mudi model checker for probabilistic validation against formal spatio-temporal specifications.

Main Results:

A methodology for automatic validation of computational models based on spatial and temporal properties was developed and implemented.
The Probabilistic Bounded Linear Spatial Temporal Logic effectively captures changes in spatial and numeric properties over time.
The Mudi model checker probabilistically determines if formal spatio-temporal specifications hold for computational models.
The approach was demonstrated through case studies on bacterial colony growth and cell chemotaxis.

Conclusions:

The Mudi platform provides a formal methodology for validating computational models against spatio-temporal logic properties.
This work is a precursor for developing and validating more complex multidimensional and multiscale models.
The developed methodology enhances the reliability of computational models for biological research and potential clinical applications.