Model Checking Optimal Infinite-Horizon Control for Probabilistic Gene Regulatory Networks

Genetic regulatory networks (GRNs) are significant fundamental biological networks through which biological system functions can be regulated. A significant challenge in the field of system biology is the construction of a control theory of GRNs through the application of external intervention controls; currently, context-sensitive probabilistic Boolean networks with perturbation (CS-PBNp) are used as an important network model in research on the optimal GRN control problem. This paper proposes an approximate optimal control strategy approach to the infinite-horizon optimal control problem based on probabilistic model checking and genetic algorithms (GAs). The proposed method first reduces the expected cost defined under the infinite-horizon control to a steady-state reward within a discrete-time Markov chain. A CS-PBNp model with a stationary control policy is then constructed to represent the cost of the fixed control strategy based on a temporal logic with a reward property, and calculations are carried out automatically by a PRISM model checker. The stationary control policy is then encoded as an element of the solution space of a GA. Based on the fitness of each control policy element as calculated by PRISM, an optimal solution can be obtained by using a GA to execute genetic operations iteratively. The experimental results generated by applying the proposed approach to the WNT5A network validate the accuracy and effectiveness of the approach.