Spatio-temporal Model Checking for 3D Individual-Based Biofilm Simulations

Individual-based microbial modelling (IbM) is a bottom-up approach to study how the heterogeneity of individual microorganisms and their local interactions influence the behaviour of microbial communities.In IbM, microbes are represented as particles endowed with a set of biological and physical attributes. These attributes are affected by both intra- and extra-cellular processes resulting in the emergence of complex spatial and temporal behaviours, such as the morphology of microbial colonies. However, the quantitative and qualitative analysis of such behaviours is difficult and often relies on visual inspection of large quantities of simulation data or on the implementation of sophisticated algorithms for data analysis. In this work, we aim to alleviate the problem by applying SSTL (Signal Spatio-Temporal Logic) model checking to formally analyse the spatial and temporal properties of 3D microbial simulations (so-called traces). Complex behaviours can be then described by simple logical formulas and automatically verified by a model checker. We apply SSTL to analyse several outstanding spatio-temporal behaviours regarding biofilm systems, including biofilm surface dynamics, their detachment and deformation under fluid conditions.