Sara Riva

Maximilien Gadouleau, Loïc Paulevé, Sara Riva

Boolean networks are extensively applied as models of complex dynamical systems, aiming at capturing essential features related to causality and synchronicity of the state changes of components along time. Dynamics of Boolean networks result from the application of their Boolean map according to a so-called update mode, specifying the possible transitions between network configurations. In this paper, we explore update modes that possess a memory on past configurations, and provide a generic framework to define them. We show that recently introduced modes such as the most permissive and interval modes can be naturally expressed in this framework, and we propose novel update modes, the history-based, trapping, and subcube-based modes. Building on the unified definitions, we provide a comprehensive comparison of memory-based update modes, resulting in their hierarchy by simulation and weak simulation. Finally, we highlight consequences of introducing memory on the notions of trajectory and attractors.

Sara Riva, Jean-Marie Lagniez, Gustavo Magaña López et al.

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. In this paper, 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 ($\exists\forall\exists$). In this paper, we introduce a Counter-Example Guided Refinement Abstraction (CEGAR) to efficiently solve these problems by coupling the resolution of two simpler formulas. We provide a prototype relying on Answer-Set Programming for each formula and show its tractability on a wide range of Boolean models of biological networks.