A logic of behaviour in context

We present a succinct, but naive, model-checking algorithm and then show how this can be improved. We investigate the complexity of model-checking, where repeated ODE solving emerges as a particular cost; assess some limitations of the technique; and identify potential routes to overcome these.