A semantics for Boolean networks consistent with regulatory threshold constraints.

Modeling biological systems with Boolean networks (BNs) is a well-established approach that enables reasoning about the qualitative dynamics of such systems, such as gene and signaling networks. Several semantics for BNs, i.e., scheduling of component updates, have been proposed that can significantly affect the predicted dynamic behaviors. The synchronous and asynchronous ones are the most popular, but they fail to capture some of the behaviors observed in reality and accounted for by quantitative models. Recently, the most permissive semantics has been introduced, guaranteed not to miss any behavior achievable by a quantitative model following the same logic as the BN, and, in addition, significantly reducing the computational complexity of dynamical analysis. But this time, it appears too permissive and tolerates spurious behaviors in many real situations. After clarifying the relationships between existing semantics, we define the threshold semantics whose dynamic behaviors are all those given by a single threshold network, a subclass of multivalued networks, for any possible threshold map. The spurious behaviors are excluded by the threshold semantics, whose qualitative behaviors appear as a proper abstraction of real biological processes founded on activation and inhibition influences regulated by single thresholds whose values are unknown, which is generally the case. We show that threshold semantics is stricter (for reachability between Boolean configurations) than the cuttable extended semantics (called here linear semantics) and stricter than a given constrained version of the most permissive semantics. We then seek to operationalize this threshold semantics. For this, we equip the constrained version of the most permissive semantics with a system of symbolic constraints, attached to any given trajectory and verifiable by a satisfiability solver. The satisfiability of this set of constraints ensures the consistency of the formal threshold conditions associated with the transitions along the trajectory. It defines a new operational semantics at the level of trajectories. Then we prove that this semantics is equivalent to the threshold semantics. Finally, we prove that the computational complexity of this semantics is the same as that of classical semantics, i.e., PSPACE, and we state several conjectures for future work.