Model Checking in Biology

Model checking is a technique to check whether programs and designs satisfy properties expressed in temporal logic. Such properties characterize sequences of events. In recent years, model checking has become a familiar tool in software and hardware industries. One of the main strengths of model checking is its ability to supply counter examples: in case that the property is not satisfied by the model we get an execution exhibiting this failure. Counter examples are fundamental in understanding, localizing, and eventually fixing, faults. This, together with the relative ease of use of model checking, led to its adoption. The success of model checking prompted system biologists to harness it to their needs. In this domain, the main usage is to have a model representing a certain biological phenomenon and to use model checking for one of two things. Either prove that the model satisfies a set of properties, i.e., reproduces a set of biological behaviors. Or to use model checking to extract interesting behaviors of the model by looking for a counter example to the property saying that this interesting behaviour does not happen. In this chapter we present the technique of model checking and survey its usage in systems biology. We take quite a liberal interpretation of what is model checking and consider also cases where the techniques underlying model checking are used for similar purposes in systems biology.