Level: M2
Contact: Philippe Dague (pdague@lmf.cnrs.fr) and Thomas Chatain (chatain@lmf.cnrs.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Boolean Networks, Constraint satisfiability
Context
Since their introduction in the late 1960s [9], logical models, such as Boolean Networks (BNs), have been widely adopted for reasoning about signaling and gene networks as they require few parameters and can easily integrate information from omics datasets and genetic screens. These models represent processes with a high degree of generalization and can offer coarse-grained but robust predictions, which makes them particularly suitable for large biological networks. BNs are formal discrete dynamical systems with notorious applications for modeling cellular differentiation and fate decision processes: the attractors capture the stable behaviors, and the trajectories capture the transient dynamics of the cell. To each BN is attached its interaction graph that references the positive and negative influences between components and hence is a compact and static abstraction of the BN dynamics [6]. Also, methods based on a generalization of the steady state notion, the so- called trap spaces, can be exploited to investigate attractor properties as well as for model reduction techniques [3].
Given a BN, i.e., n local functions from Bn to B, where B = {0, 1} is the Boolean domain, the update mode specifies how to compute the next configuration from the present one. There is a vast zoo of update modes [1, 7], but traditionally, two modes are usually considered in biological modeling: the synchronous (or parallel) deterministic mode, where the next configuration results from the simultaneous application of all n local functions, and the fully asynchronous, where the next configuration results from the application of only one local function, chosen non-deterministically. However, (a)synchronous update modes do not lead to a complete qualitative abstraction of quantitative systems and preclude the prediction of trajectories that are actually feasible when considering time scales or concentration scales. The Most Permissive (MP) [5, 8] is a recently introduced update mode that brings the formal guarantee to capture any trajectory that is feasible by any quantitative system compatible with the Boolean network. In addition, the MP update mode benefits from much better complexity results than the traditional update modes for all current problems, e.g., the problem of reachability between configurations, which is PSPACE-complete for the latter ones, becomes P N P (even P with a local monotonicity assumption) for it.
Despite its good properties, the MP update mode sometimes appears “too permissive”, and it is also the case of the stricter linearly-cuttable update [4]. Allowing spurious, i.e., not feasible in practice, behaviors is quite normal for any abstraction of a given problem; nevertheless, one would want to eliminate the most obvious of them. In particular, those that are not consistent with respect to the “local context, i.e., that differ at two different occurrences of the same context. For example, it may appear legitimate to require that an (unknown but fixed) order is maintained, inside any given component, between the thresholds of activation/inhibition by this component of all the components it influences, or else a fixed time order of the crossing of those thresholds by the variables involved along the trajectory, all else being equal.
The recent work [2] addresses this issue by defining 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, and by characterizing it operationally by adding to the MP update mode a system of symbolic constraints, attached to any given trajectory and verifiable by a sat- isfiability solver. The satisfiability of this set of constraints ensures the consistency of the formal threshold conditions associated with the transitions along the trajectory.
Objectives
The objective is to complete the work [2], which in particular contains several conjectures to be proven or disproven by counterexamples. And to implement the satisfiability checking of the system of symbolic constraints associated with any trajectory, and to automate the construction of such consistent trajectories. With the goal of helping in the discovery of counterexamples or of giving insights for establishing proofs, but also of exploring the real complexity of the update mode on realistic examples, and of studying trap spaces
Requirements
Skills in formal methods. Knowledge to acquire about BNs (at least by reading [2], which is self- contained). Use of a logic-based programming language for experimentation, such as ASP (Answer Set Programming).
Supervision
Philippe Dague, emeritus professor at Université Paris-Saclay (philippe.dague@universite-paris- saclay.fr) and Thomas Chatain, associate professor HDR at ENS Paris-Saclay (thomas.chatain@ens- paris-saclay.fr).
References
[1] Thomas Chatain, Stefan Haar, Juraj Kolčák, Lo¨ıc Paulevé, and Aalok Thakkar. “Concurrency in Boolean networks”. In: Natural Computing 19.1 (2020), pp. 91–109.
[2] Philippe Dague. A semantics for Boolean networks consistent with regulatory threshold constraints.
Submitted in 2025 to Journal of Theoretical Biology,
[3] Hannes Klarner, Alexander Bockmayr, and Heike Siebert. “Computing maximal and minimal trap spaces of Boolean networks”. In: Natural Computing 14.4 (2015), pp. 535–544.
[4] Aurélien Naldi, Adrien Richard, and Elisa Tonello. “Linear cuts in Boolean network”. In: Natural Computing 22(3) (2023), pp. 431–451.
[5] Loïc Paulevé, Juraj Kolčák, Thomas Chatain, and Stefan Haar. “Reconciling qualitative, abstract, and scalable modeling of biological networks”. In: Nature Communications 11.1 (2020), p. 4256.
[6] Loïc Paulevé and Adrien Richard. “Static analysis of Boolean networks based on interaction graphs: a survey”. In: Electronic Notes in Theoretical Computer Science 284 (2012), pp. 93–104.
[7] Loïc Paulevé and Sylvain Sené. “Boolean networks and their dynamics: the impact of updates”. In: Systems Biology Modelling and Analysis: Formal Bioinformatics Methods and Tools. Wiley, 2022.
[8] Loïc Paulevé and Sylvain Sené. “Non-Deterministic Updates of Boolean Networks”. In: 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021). Ed. by Alonso Castillo-Ramirez, Pierre Guillon, and Kévin Perrot. Vol. 90. Open Access Series in Informatics (OASIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, 10:1–10:16.
[9] René Thomas. “Boolean formalization of genetic control circuits”. In: Journal of theoretical biology 42.3 (1973), pp. 563–585.