A symbolic approach to probabilistic verification of boolean networks

A Boolean network (BN) is well known as one of the models of biological networks such as gene regulatory networks, and has been extensively studied. In this paper, for a BN, the verification problems such as the reachability problem are discussed. First, a probabilistic model including both synchronous and asynchronous Boolean dynamics is derived. This model can be generalized as a probabilistic BN. Next, a solution method of the verification problems is proposed, based on a model checking technique. Finally, our method is applied to an apoptosis network. The proposed approach provides us an easy and convenient tool for analysis and control of biological networks.