is an approximate probabilistic multiscale multidimensional spatio-temporal meta model checker used for the validation of computational models relative to a given formal specification. A diagram of the model checking process is provided below.

A Mule model checker instance validates models against formal specifications comprising multiscale multidimensional spatio-temporal logic properties. If a model is valid the model checker execution finishes with the answer Yes (true), otherwise No (false). In the latter case a set of counterexample simulation traces is additionally provided as output which can be reproduced in a step-by-step manner using a simulator, and enable locating modelling errors and potentially debugging them.