Finding Attractors in Synchronous Multiple-Valued Networks Using SAT-based Bounded Model Checking

摘要

Synchronous multiple-valued networks are a discrete-space discrete-time model of gene regulatory networks. Theircycle of states, called attractors, are believed to give a good indication of the possible functional modes of the system. This motivates research on algorithms for finding attractors. Existing decision diagram-based approaches have limited capacity due to the excessive memory requirements of decision diagrams. Simulation-based approaches can be applied to larger networks, however, they are incomplete. We present an algorithm which uses a SAT-based bounded model checking approach to find all allractors in a multiple-valued network. The efficiency of the presented algorithm is evaluated by analyzing 30 network models of real biological processes as well as 35.000 randomly generated 4-valued networks. The results show that our algorithm has a potential to handle an order of magnitude larger models than currently possible.