is a multidimensional pseudo-3D spatio-temporal model checker employed for the formal validation of computational models. A diagram of the model checking process is provided below.

Mudi automatically validates a model against a formal specification comprising spatio-temporal logic properties. If the model is valid (Yes) then the execution finishes directly. Otherwise (No) a counter-example simulation trace is provided in order to be able to replicate the execution using a simulator, locating the error and potentially debugging it.

The model checker was validated against the phase variation patterning in bacterial colonies growth and chemotactic aggregation of cells (chemotaxis) case studies.

Related publication:

Ovidiu Pârvu and David Gilbert, Automatic validation of computational models using pseudo-3D spatio-temporal model checking, BMC Systems Biology, vol. 8, no. 1, p. 124, Dec. 2014 (Open Access)