Reachability analysis of probabilistic Boolean networks using model checking

A probabilistic Boolean network (PBN) is one of the significant models of biological networks such as gene regulatory networks, and has been extensively studied. In analysis and control of PBNs, it is necessary to compute the state transition diagram with 2ⁿ nodes for a given PBN with n states. In this paper, to avoid this computation, a model checking approach for solving the reachability problem is proposed. In the proposed method, Boolean functions in PBNs are directly used, and an implementation using the model checker PRISM is easy.