Abstract
A context-sensitive probabilistic Boolean network with perturbation (CS-PBNp) closely models gene regulatory networks under external controls that alter the evolution of the networks in a desirable way over a finite time horizon. In this paper, we consider optimal control for a CS-PBNp, proposing an approach, based on a formal verification technique - probabilistic model checking, for finding optimal control policy that minimizes the expected cost over the entire control horizon. To this end, we first present a detailed procedure of modeling a CS-PBNp using the modeling language of a widely used probabilistic model checker PRISM. Furthermore, by analyzing computation of reward-based temporal properties, we provide a reduction approach allowing us to formulate the optimal control problem as minimum reachability reward properties. Based on this result, we incorporate control and state cost information into the PRISM code of a CS-PBNp such that automated model checking a minimum reachability reward property on the code gives the solution to the optimal control problem. Experiment results on an apoptosis network demonstrate the feasibility and effectiveness of our approach.