Symbolic approach to verification and control of deterministic/probabilistic Boolean networks

Area of Science:

• Computational Biology
• Systems Biology
• Network Science

Background:

• Boolean networks (BNs) are established models for biological systems, particularly gene regulatory networks.
• Verification and control problems in BNs are crucial for understanding network dynamics.
• Existing methods may lack flexibility in handling synchronous and asynchronous dynamics.

Purpose of the Study:

• To develop a generalized probabilistic Boolean network (BN) model.
• To propose a novel method for verification and control problems in BNs.
• To provide a convenient tool for analyzing and controlling biological networks.

Main Methods:

• Derivation of a probabilistic model encompassing both synchronous and asynchronous Boolean dynamics.
• Generalization of the model into a probabilistic BN.
• Application of a probabilistic model checker, PRISM, for solving verification/control problems.

Main Results:

• A generalized probabilistic BN model was successfully derived.
• A PRISM-based solution method for BN verification/control problems was proposed.
• The method was effectively applied to apoptosis and WNT5A biological networks.

Conclusions:

• The proposed PRISM-based approach offers an accessible and efficient tool for the analysis and control of biological networks.
• This probabilistic BN model enhances the study of complex biological system dynamics.
• The findings facilitate a deeper understanding and manipulation of gene regulatory mechanisms.