Logical consequence as a tool for qualitative analysis of Boolean networks

Abstract

A new propositional model of Boolean network dynamics is proposed in which the primary relation between states is an implication. Proving the satisfiability of a dynamic property represented as a Boolean formula is reduced to proving that this formula is a logical consequence of the implication model of a Boolean network. The logical consequence problem is reduced to a Boolean satisfiability problem with ${2^n}$ unknown Boolean variables, where \textit{n} is the dimensionality of the state vector of the Boolean network. The proposed qualitative analysis technique is demonstrated for dynamic reachability and controllability properties in a Boolean network with respect to sets of initial and target states.