Model checking optimal finite-horizon control for probabilistic gene regulatory networks

Area of Science:

• Systems Biology
• Computational Biology
• Formal Verification

Background:

• Probabilistic Boolean Networks (PBNs) are used for analyzing gene regulatory networks with uncertainty.
• Context-sensitive PBNs with perturbation (CS-PBNp) better model biological systems influenced by external stimuli and perturbations.
• Optimal control for CS-PBNp is crucial for understanding and manipulating biological processes.

Purpose of the Study:

• To apply probabilistic model checking for optimal control of CS-PBNp.
• To minimize the expected cost over a finite control horizon for CS-PBNp.
• To develop a method for formulating and solving optimal control problems in gene regulatory networks.

Main Methods:

• Modeling CS-PBNp using the PRISM probabilistic model checker.
• Analyzing reward-based temporal properties and probabilistic model checking computations.
• Formulating optimal control as minimum reachability reward properties and incorporating costs into PRISM code for automated solving.

Main Results:

• A procedure for modeling CS-PBNp in PRISM was described.
• A method to formulate optimal control problems as minimum reachability reward properties was developed.
• Experiments on apoptosis and WNT5A networks demonstrated the feasibility and effectiveness of the approach.

Conclusions:

• The probabilistic model checking approach avoids explicit computation of large state transition relations.
• It provides a natural depiction of gene regulatory network dynamics and a canonical form for optimal control problems.
• This work facilitates the application of formal verification techniques in systems biology for analyzing gene regulatory networks.