Modeling and Analysis of Biological Networks with Model Checking
D. Bosnacki, P.A.J. Hilbers, R.S. Mans, and E.P. de Vink

Different formalisms and approaches exist for the modeling of biological
networks. In this chapter we focus on model checking as a method that exploits
executable models. Its main advantage is that they lend themselves to formal
verification. 

After introducing the basic concepts, we show how standard model checking can
be used to model and analyze biological systems. To this end we use as the
modeling language Promela, the specification language of the model checking
tool SPIN. The SPIN tool can be used to check a broad range of properties. In
particular, we show how SPIN can be used to detect steady states of the
biological systems as well as periodic behavior. Some of the case studies
that we discuss have also been modeled with other formalisms, like Petri nets
or π-calculus. We discuss the advantages of model checking over those
approaches. 

The next part is devoted to modeling and analysis of biological systems which
are inherently probabilistic. To this end we use a special kind of model
checking, probabilistic model checking. We demonstrate the concepts of
probabilistic model checking for biological systems using the probabilistic
model checking tool Prism.