Control and synthesis of minimal trap spaces in Boolean Network

Since recent years, we observe a surge of successful applications of Boolean networks (BNs) in biology and medicine for the modeling and prediction of cellular dynamics in the case of cancer and cellular reprogramming. Such applications face two main challenges: being able to design a qualitative Boolean model which is faithful to the behavior of the biological system and being able to compute predictions to control its (long-term) dynamics. From a computational point of view, the latter problem mostly depends on the complexity of the dynamical property to enforce, while the former additionally suffers from the combinatorics of candidate models.

Minimal trap spaces (MTSs) capture subspaces in which the Boolean dynamics is trapped, whatever the update mode. They correspond to the attractors of the most permissive mode. Due to their versatility, the computation of MTSs has recently gained traction, essentially by focusing on their enumeration. We address the logical reasoning on universal properties of MTSs in the scope of two problems: the reprogramming of Boolean networks for identifying the permanent freeze of Boolean variables that enforce a given property on all the MTSs, and the synthesis of Boolean networks from universal properties on their MTSs. Both problems reduce to solving the satisfiability of quantified propositional logic formula with 3 levels of quantifiers.