Home » model checking

Tag: model checking

How do you validate a computational model of a system evolving in time and space?

To be more specific the question should be how do you validate a computational model of a system evolving in time and space relative to a specification describing its expected behaviour? One possible answer to this question is multidimensional spatio-temporal model checking.

To explain what I mean by this let us first describe “traditional” model checking.

Model checking


Model checking is a method for automatically validating a computational model relative to a specification.


The computational model is an abstract representation of a real life system which describes how the system changes its state over time. The state of the system is described by the values of a set of state variables. Therefore in more abstract terms a computational model describes how a set of state variables change their value over time.

The specification comprises a collection of statements encoded in formal languages which can describe how the state of a system changes over time. Such languages are called temporal logics. The reason for employing temporal logics instead of natural languages (e.g. English) is that the former have a fixed syntax and semantics while the latter do not (e.g. metaphors use the same words/syntax but have different semantics depending on the context in which they are used).

Each statement in the specification describes how a subset of state variables are expected to change their value over time. Therefore the model checking problem is to verify if the state variables of a system change their value over time as described in the specification by verifying all possible states of the system.


Model checking is a method employed for proving that a model is (in)valid relative to a specification because it considers all possible states of the system. This is in contrast to testing based approaches which can only show the presence but not the absence of errors in a model because they usually consider only a subset of the possible system states.

Multidimensional model checking

Traditional model checking approaches usually assume that the state of the system can be represented by a set of real-valued state variables. Consequently the employed temporal logics contain language constructs which enable reasoning about real values (e.g. arithmetic operators +, -, *, /).

However in case of systems which evolve both in time and space there is an additional need to represent the state of the system using multidimensional state variables (e.g. a matrix representing a discretised 2D space). Moreover the employed temporal logic should additionally contain spatial functions which enable reasoning about how geometric properties (e.g. area) of the systems change over time.

In order to address this issue multidimensional spatio-temporal model checking was developed. The main extra features of multidimensional spatio-temporal compared to traditional model checking are:

  • Multidimensional state variables for encoding space;
  • Functions for automatically computing geometric properties of the system at a given state;
  • A quantitative spatio-temporal logic which extends traditional temporal logics with space related functions.

If interested in a more rigurous scientific description of multidimensional model checking please visit the recently published open access paper and website. Examples of the potential impact multidimensional model checking could have on industry are given on my personal PhD project research website.