CHAPTER 39
MODELING AND ANALYSIS OF BIOLOGICAL NETWORKS WITH MODEL CHECKING
Dragan Bošna
ki, Peter A.J. Hilbers, Ronny S. Mans, and Erik P. de Vink
39.1 INTRODUCTION
During last decades, biological networks, like signal transduction pathways, meta-bolic pathways, and genetic networks, have received increasing attention in biochemistry. In each living organism, a growing plethora of such networks have been identified. It has become clear that the understanding of the mechanisms and their functioning is crucial for elucidating the functioning of the cell and the organism as a whole.
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. Standard simulation on the model can only yield predictions regarding model properties with certain probability. The advantage of model checking over standard simulation is that it considers all possible behaviors of the systems, not just some subset of it and therefore yields conclusions with certainty.
After intrducing the basic concepts in the next section, in Section 39.3, 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 ...
