An efficient algorithm for computing fixed length attractors based on bounded model checking in synchronous Boolean networks with biochemical applications.

Genetic regulatory networks are the key to understanding biochemical systems. One condition of the genetic regulatory network under different living environments can be modeled as a synchronous Boolean network. The attractors of these Boolean networks will help biologists to identify determinant and stable factors. Existing methods identify attractors based on a random initial state or the entire state simultaneously. They cannot identify the fixed length attractors directly. The complexity of including time increases exponentially with respect to the attractor number and length of attractors. This study used the bounded model checking to quickly locate fixed length attractors. Based on the SAT solver, we propose a new algorithm for efficiently computing the fixed length attractors, which is more suitable for large Boolean networks and numerous attractors' networks. After comparison using the tool BooleNet, empirical experiments involving biochemical systems demonstrated the feasibility and efficiency of our approach.

An efficient algorithm for finding attractors in synchronous Boolean networks with biochemical applications.

Self-organized systems, genetic regulatory systems and other living systems can be modeled as synchronous Boolean networks with stable states, which are also called state-cycle attractors (SCAs). This paper summarizes three classes of SCAs and presents a new efficient binary decision diagram based algorithm to find all SCAs of synchronous Boolean networks. After comparison with the tool BooleNet, empirical experiments with biochemical systems demonstrated the feasibility and efficiency of our approach.