-
Phenotype control and elimination of variables in Boolean networks
Authors:
Elisa Tonello,
Loïc Paulevé
Abstract:
We investigate how elimination of variables can affect the asymptotic dynamics and phenotype control of Boolean networks. In particular, we look at the impact on minimal trap spaces, and identify a structural condition that guarantees their preservation. We examine the possible effects of variable elimination under three of the most popular approaches to control (attractor-based control, value pro…
▽ More
We investigate how elimination of variables can affect the asymptotic dynamics and phenotype control of Boolean networks. In particular, we look at the impact on minimal trap spaces, and identify a structural condition that guarantees their preservation. We examine the possible effects of variable elimination under three of the most popular approaches to control (attractor-based control, value propagation and control of minimal trap spaces), and under different update schemes (synchronous, asynchronous, generalized asynchronous). We provide some insights on the application of reduction, and an ample inventory of examples and counterexamples.
△ Less
Submitted 4 June, 2024;
originally announced June 2024.
-
Bringing memory to Boolean networks: a unifying framework
Authors:
Maximilien Gadouleau,
Loïc Paulevé,
Sara Riva
Abstract:
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 pa…
▽ More
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. We propose novel update modes, the history-based and trap** modes, and provide a comprehensive comparison between them. Furthermore, we show that trap** dynamics, which further generalize the most permissive mode, correspond to a rich class of networks related to transitive dynamics and encompassing commutative networks. Finally, we provide a thorough characterization of the structure of minimal and principal trapspaces, bringing a combinatorial and algebraic understanding of these objects.
△ Less
Submitted 4 April, 2024;
originally announced April 2024.
-
mpbn: a simple tool for efficient edition and analysis of elementary properties of Boolean networks
Authors:
Van-Giang Trinh,
Belaid Benhamou,
Loïc Paulevé
Abstract:
The tool mpbn offers a Python programming interface for an easy interactive editing of Boolean networks and the efficient computation of elementary properties of their dynamics, including fixed points, trap spaces, and reachability properties under the Most Permissive update mode. Relying on Answer-Set Programming logical framework, we show that mpbn is scalable to models with several thousands of…
▽ More
The tool mpbn offers a Python programming interface for an easy interactive editing of Boolean networks and the efficient computation of elementary properties of their dynamics, including fixed points, trap spaces, and reachability properties under the Most Permissive update mode. Relying on Answer-Set Programming logical framework, we show that mpbn is scalable to models with several thousands of nodes and is one of the best-performing tool for computing minimal and maximal trap spaces of Boolean networks, a key feature for understanding and controling their stable behaviors. The tool is available at https://github.com/bnediction/mpbn.
△ Less
Submitted 10 March, 2024;
originally announced March 2024.
-
Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks
Authors:
Sara Riva,
Jean-Marie Lagniez,
Gustavo Magaña López,
Loïc Paulevé
Abstract:
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 tw…
▽ More
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.
△ Less
Submitted 20 July, 2023; v1 submitted 3 May, 2023;
originally announced May 2023.
-
Attractor identification in asynchronous Boolean dynamics with network reduction
Authors:
Elisa Tonello,
Loïc Paulevé
Abstract:
Identification of attractors, that is, stable states and sustained oscillations, is an important step in the analysis of Boolean models and exploration of potential variants. We describe an approach to the search for asynchronous cyclic attractors of Boolean networks that exploits, in a novel way, the established technique of elimination of components. Computation of attractors of simplified netwo…
▽ More
Identification of attractors, that is, stable states and sustained oscillations, is an important step in the analysis of Boolean models and exploration of potential variants. We describe an approach to the search for asynchronous cyclic attractors of Boolean networks that exploits, in a novel way, the established technique of elimination of components. Computation of attractors of simplified networks allows the identification of a limited number of candidate attractor states, which are then screened with techniques of reachability analysis combined with trap space computation. An implementation that brings together recently developed Boolean network analysis tools, tested on biological models and random benchmark networks, shows the potential to significantly reduce running times.
△ Less
Submitted 2 May, 2023;
originally announced May 2023.
-
Computational Complexity of Minimal Trap Spaces in Boolean Networks
Authors:
Kyungduk Moon,
Kangbok Lee,
Loïc Paulevé
Abstract:
A Boolean network (BN) is a discrete dynamical system defined by a Boolean function that maps to the domain itself. A trap space of a BN is a generalization of a fixed point, which is defined as the sub-hypercubes closed by the function of the BN. A trap space is minimal if it does not contain any smaller trap space. Minimal trap spaces have applications for the analysis of attractors of BNs with…
▽ More
A Boolean network (BN) is a discrete dynamical system defined by a Boolean function that maps to the domain itself. A trap space of a BN is a generalization of a fixed point, which is defined as the sub-hypercubes closed by the function of the BN. A trap space is minimal if it does not contain any smaller trap space. Minimal trap spaces have applications for the analysis of attractors of BNs with various update modes. This paper establishes the computational complexity results of three decision problems related to minimal trap spaces: the decision of the trap space property of a sub-hypercube, the decision of its minimality, and the decision of the membership of a given configuration to a minimal trap space. Under several cases on Boolean function representations, we investigate the computational complexity of each problem. In the general case, we demonstrate that the trap space property is coNP-complete, and the minimality and the membership properties are $Π_2^{\text P}$-complete. The complexities drop by one level in the polynomial hierarchy whenever the local functions of the BN are either unate, or are represented using truth-tables, binary decision diagrams, or double DNFs (Petri net encoding): the trap space property can be decided in a polynomial time, whereas deciding the minimality and the membership are coNP- complete. When the BN is given as its functional graph, all these problems are in P.
△ Less
Submitted 14 March, 2023; v1 submitted 24 December, 2022;
originally announced December 2022.
-
Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets
Authors:
Giann Karlo Aguirre-Samboní,
Stefan Haar,
Loïc Paulevé,
Stefan Schwoon,
Nick Würdemann
Abstract:
A crucial question in analyzing a concurrent system is to determine its long-run behaviour, and in particular, whether there are irreversible choices in its evolution, leading into parts of the reachability space from which there is no return to other parts. Casting this problem in the unifying framework of safe Petri nets, our previous work has provided techniques for identifying attractors, i.e…
▽ More
A crucial question in analyzing a concurrent system is to determine its long-run behaviour, and in particular, whether there are irreversible choices in its evolution, leading into parts of the reachability space from which there is no return to other parts. Casting this problem in the unifying framework of safe Petri nets, our previous work has provided techniques for identifying attractors, i.e. terminal strongly connected components of the reachability space, whose attraction basins we wish to determine. Here, we provide a solution for the case of safe Petri nets. Our algorithm uses net unfoldings and provides a map of all of the system's configurations (concurrent executions) that act as cliff-edges, i.e. any maximal extension for those configurations lies in some basin that is considered fatal. The computation turns out to require only a relatively small prefix of the unfolding, just twice the depth of Esparza's complete prefix.
△ Less
Submitted 21 September, 2022;
originally announced September 2022.
-
Marker and source-marker reprogramming of Most Permissive Boolean networks and ensembles with BoNesis
Authors:
Loïc Paulevé
Abstract:
Boolean networks (BNs) are discrete dynamical systems with applications to the modeling of cellular behaviors. In this paper, we demonstrate how the software BoNesis can be employed to exhaustively identify combinations of perturbations which enforce properties on their fixed points and attractors. We consider marker properties, which specify that some components are fixed to a specific value. We…
▽ More
Boolean networks (BNs) are discrete dynamical systems with applications to the modeling of cellular behaviors. In this paper, we demonstrate how the software BoNesis can be employed to exhaustively identify combinations of perturbations which enforce properties on their fixed points and attractors. We consider marker properties, which specify that some components are fixed to a specific value. We study 4 variants of the marker reprogramming problem: the reprogramming of fixed points, of minimal trap spaces, and of fixed points and minimal trap spaces reachable from a given initial configuration with the most permissive update mode. The perturbations consist of fixing a set of components to a fixed value. They can destroy and create new attractors. In each case, we give an upper bound on their theoretical computational complexity, and give an implementation of the resolution using the BoNesis Python framework. Finally, we lift the reprogramming problems to ensembles of BNs, as supported by BoNesis, bringing insight on possible and universal reprogramming strategies. This paper can be executed and modified interactively.
△ Less
Submitted 14 March, 2023; v1 submitted 27 July, 2022;
originally announced July 2022.
-
Variable-Depth Simulation of Most Permissive Boolean Networks
Authors:
Théo Roncalli,
Loïc Paulevé
Abstract:
In systems biology, Boolean networks (BNs) aim at modeling the qualitative dynamics of quantitative biological systems. Contrary to their (a)synchronous interpretations, the Most Permissive (MP) interpretation guarantees capturing all the trajectories of any quantitative system compatible with the BN, without additional parameters. Notably, the MP mode has the ability to capture transitions relate…
▽ More
In systems biology, Boolean networks (BNs) aim at modeling the qualitative dynamics of quantitative biological systems. Contrary to their (a)synchronous interpretations, the Most Permissive (MP) interpretation guarantees capturing all the trajectories of any quantitative system compatible with the BN, without additional parameters. Notably, the MP mode has the ability to capture transitions related to the heterogeneity of time scales and concentration scales in the abstracted quantitative system and which are not captured by asynchronous modes. So far, the analysis of MPBNs has focused on Boolean dynamical properties, such as the existence of particular trajectories or attractors. This paper addresses the sampling of trajectories from MPBNs in order to quantify the propensities of attractors reachable from a given initial BN configuration. The computation of MP transitions from a configuration is performed by iteratively discovering possible state changes. The number of iterations is referred to as the permissive depth, where the first depth corresponds to the asynchronous transitions. This permissive depth reflects the potential concentration and time scales heterogeneity along the abstracted quantitative process. The simulation of MPBNs is illustrated on several models from the literature, on which the depth parametrization can help to assess the robustness of predictions on attractor propensities changes triggered by model perturbations.
△ Less
Submitted 25 June, 2022;
originally announced June 2022.
-
BioSimulators: a central registry of simulation engines and services for recommending specific tools
Authors:
Bilal Shaikh,
Lucian P. Smith,
Dan Vasilescu,
Gnaneswara Marupilla,
Michael Wilson,
Eran Agmon,
Henry Agnew,
Steven S. Andrews,
Azraf Anwar,
Moritz E. Beber,
Frank T. Bergmann,
David Brooks,
Lutz Brusch,
Laurence Calzone,
Kiri Choi,
Joshua Cooper,
John Detloff,
Brian Drawert,
Michel Dumontier,
G. Bard Ermentrout,
James R. Faeder,
Andrew P. Freiburger,
Fabian Fröhlich,
Akira Funahashi,
Alan Garny
, et al. (46 additional authors not shown)
Abstract:
Computational models have great potential to accelerate bioscience, bioengineering, and medicine. However, it remains challenging to reproduce and reuse simulations, in part, because the numerous formats and methods for simulating various subsystems and scales remain siloed by different software tools. For example, each tool must be executed through a distinct interface. To help investigators find…
▽ More
Computational models have great potential to accelerate bioscience, bioengineering, and medicine. However, it remains challenging to reproduce and reuse simulations, in part, because the numerous formats and methods for simulating various subsystems and scales remain siloed by different software tools. For example, each tool must be executed through a distinct interface. To help investigators find and use simulation tools, we developed BioSimulators (https://biosimulators.org), a central registry of the capabilities of simulation tools and consistent Python, command-line, and containerized interfaces to each version of each tool. The foundation of BioSimulators is standards, such as CellML, SBML, SED-ML, and the COMBINE archive format, and validation tools for simulation projects and simulation tools that ensure these standards are used consistently. To help modelers find tools for particular projects, we have also used the registry to develop recommendation services. We anticipate that BioSimulators will help modelers exchange, reproduce, and combine simulations.
△ Less
Submitted 13 March, 2022;
originally announced March 2022.
-
Non-deterministic updates of Boolean networks
Authors:
Loïc Paulevé,
Sylvain Sené
Abstract:
Boolean networks are discrete dynamical systems where each automaton has its own Boolean function for computing its state according to the configuration of the network. The updating mode then determines how the configuration of the network evolves over time. Many of updating modes from the literature, including synchronous and asynchronous modes, can be defined as the composition of elementary det…
▽ More
Boolean networks are discrete dynamical systems where each automaton has its own Boolean function for computing its state according to the configuration of the network. The updating mode then determines how the configuration of the network evolves over time. Many of updating modes from the literature, including synchronous and asynchronous modes, can be defined as the composition of elementary deterministic configuration updates, i.e., by functions map** configurations of the network. Nevertheless, alternative dynamics have been introduced using ad-hoc auxiliary objects, such as that resulting from binary projections of Memory Boolean networks, or that resulting from additional pseudo-states for Most Permissive Boolean networks. One may wonder whether these latter dynamics can still be classified as updating modes of finite Boolean networks, or belong to a different class of dynamical systems. In this paper, we study the extension of updating modes to the composition of non-deterministic updates, i.e., map** sets of finite configurations. We show that the above dynamics can be expressed in this framework, enabling a better understanding of them as updating modes of Boolean networks. More generally, we argue that non-deterministic updates pave the way to a unifying framework for expressing complex updating modes, some of them enabling transitions that cannot be computed with elementary and non-elementary deterministic updates.
△ Less
Submitted 29 June, 2021;
originally announced June 2021.
-
SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers
Authors:
Gilles Audemard,
Loïc Paulevé,
Laurent Simon
Abstract:
SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. Moreover, there has been more than a thousand solvers published so far, some of them releas…
▽ More
SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. Moreover, there has been more than a thousand solvers published so far, some of them released in the early 90's. If the SAT community wants to archive and be able to keep track of all the solvers that made its history, it urgently needs to deploy an important effort. We propose to initiate a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far. We rely on the best tools for archiving and building binaries (thanks to Docker, GitHub and Zenodo) and provide a consistent and easy way for this. Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.
△ Less
Submitted 2 June, 2020;
originally announced June 2020.
-
Synthesis of Boolean Networks from Biological Dynamical Constraints using Answer-Set Programming
Authors:
Stéphanie Chevalier,
Christine Froidevaux,
Loïc Paulevé,
Andrei Zinovyev
Abstract:
Boolean networks model finite discrete dynamical systems with complex behaviours. The state of each component is determined by a Boolean function of the state of (a subset of) the components of the network. This paper addresses the synthesis of these Boolean functions from constraints on their domain and emerging dynamical properties of the resulting network. The dynamical properties relate to the…
▽ More
Boolean networks model finite discrete dynamical systems with complex behaviours. The state of each component is determined by a Boolean function of the state of (a subset of) the components of the network. This paper addresses the synthesis of these Boolean functions from constraints on their domain and emerging dynamical properties of the resulting network. The dynamical properties relate to the existence and absence of trajectories between partially observed configurations, and to the stable behaviours (fixpoints and cyclic attractors). The synthesis is expressed as a Boolean satisfiability problem relying on Answer-Set Programming with a parametrized complexity, and leads to a complete non-redundant characterization of the set of solutions. Considered constraints are particularly suited to address the synthesis of models of cellular differentiation processes, as illustrated on a case study. The scalability of the approach is demonstrated on random networks with scale-free structures up to 100 to 1,000 nodes depending on the type of constraints.
△ Less
Submitted 27 February, 2020; v1 submitted 10 September, 2019;
originally announced September 2019.
-
Concurrency in Boolean networks
Authors:
Thomas Chatain,
Stefan Haar,
Juraj Kolčák,
Loïc Paulevé,
Aalok Thakkar
Abstract:
Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of component updates can have a dramatic impact on the predicted behaviours. In this paper, we explore the use of Read (contextual) Petri Nets (RPNs) to study dynamics of BNs…
▽ More
Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of component updates can have a dramatic impact on the predicted behaviours. In this paper, we explore the use of Read (contextual) Petri Nets (RPNs) to study dynamics of BNs from a concurrency theory perspective. After showing bi-directional translations between RPNs and BNs and analogies between results on synchronism sensitivity, we illustrate that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly conclude on the absence/impossibility of reaching specific configurations. We propose an encoding of BNs capitalizing on the RPN semantics enabling more behaviour than the generalized asynchronous updating mode. The proposed encoding ensures a correct abstraction of any multivalued refinement, as one may expect to achieve when modelling biological systems with no assumption on its time features.
△ Less
Submitted 31 May, 2019;
originally announced May 2019.
-
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
Authors:
Stefan Haar,
Juraj Kolčák,
Loïc Paulevé
Abstract:
Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while parameterising the precise rules for drawing the possible temporal evolutions of the states of the components. A key chall…
▽ More
Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while parameterising the precise rules for drawing the possible temporal evolutions of the states of the components. A key challenge is then to identify the discrete parameters corresponding to concrete models with desired dynamical properties. This paper addresses the restriction of the abstract execution of parametric regulatory (discrete) networks by the means of static analysis of reachability properties (goal states). Initially defined at the level of concrete parameterised models, the goal-oriented reduction of dynamics is lifted to parametric networks, and is proven to preserve all the minimal traces to the specified goal states. It results that one can jointly perform the refinement of parametric networks (restriction of domain of parameters) while reducing the necessary transitions to explore and preserving reachability properties of interest.
△ Less
Submitted 29 November, 2018;
originally announced November 2018.
-
Most Permissive Semantics of Boolean Networks
Authors:
Thomas Chatain,
Stefan Haar,
Juraj Kol{č}ák,
Loïc Paulevé
Abstract:
As shown in (http://dx.doi.org/10.1101/2020.03.22.998377), the usual update modes of Boolean networks (BNs), including synchronous and (generalized) asynchronous, fail to capture behaviors introduced by multivalued refinements. Thus, update modes do not allow a correct abstract reasoning on dynamics of biological systems, as they may lead to reject valid BN models.This technical report lists the m…
▽ More
As shown in (http://dx.doi.org/10.1101/2020.03.22.998377), the usual update modes of Boolean networks (BNs), including synchronous and (generalized) asynchronous, fail to capture behaviors introduced by multivalued refinements. Thus, update modes do not allow a correct abstract reasoning on dynamics of biological systems, as they may lead to reject valid BN models.This technical report lists the main definitions and properties of the most permissive semantics of BNs introduced in http://dx.doi.org/10.1101/2020.03.22.998377. This semantics meets with a correct abstraction of any multivalued refinements, with any update mode. It subsumes all the usual updating modes, while enabling new behaviors achievable by more concrete models. Moreover, it appears that classical dynamical analyzes of reachability and attractors have a simpler computational complexity:- reachability can be assessed in a polynomial number of iterations. The computation of iterations is in NP in the very general case, and is linear when local functions are monotonic, or with some usual representations of functions of BNs (binary decision diagrams, Petri nets, automata networks, etc.). Thus, reachability is in P with locally-monotonic BNs, and P$^{\text{NP}}$ otherwise (instead of being PSPACE-complete with update modes);- deciding wherever a configuration belongs to an attractor is in coNP with locally-monotonic BNs, and coNP$^{\text{coNP}}$ otherwise (instead of PSPACE-complete with update modes).Furthermore, we demonstrate that the semantics completely captures any behavior achievable with any multilevel or ODE refinement of the BN; and the semantics is minimal with respect to this model refinement criteria: to any most permissive trajectory, there exists a multilevel refinement of the BN which can reproduce it.In brief, the most permissive semantics of BNs enables a correct abstract reasoning on dynamics of BNs, with a greater tractability than previously introduced update modes.
△ Less
Submitted 8 April, 2020; v1 submitted 30 August, 2018;
originally announced August 2018.
-
Parameter Space Abstraction and Unfolding Semantics of Discrete Regulatory Networks
Authors:
Juraj Kolčák,
David Šafránek,
Stefan Haar,
Loïc Paulevé
Abstract:
The modelling of discrete regulatory networks combines a graph specifying the pairwise influences between the variables of the system, and a parametrisation from which can be derived a discrete transition system. Given the influence graph only, the exploration of admissible parametrisations and the behaviours they enable is computationally demanding due to the combinatorial explosions of both para…
▽ More
The modelling of discrete regulatory networks combines a graph specifying the pairwise influences between the variables of the system, and a parametrisation from which can be derived a discrete transition system. Given the influence graph only, the exploration of admissible parametrisations and the behaviours they enable is computationally demanding due to the combinatorial explosions of both parametrisation and reachable state space.
This article introduces an abstraction of the parametrisation space and its refinement to account for the existence of given transitions, and for constraints on the sign and observability of influences. The abstraction uses a convex sublattice containing the concrete parametrisation space specified by its infimum and supremum parametrisations. It is shown that the computed abstractions are optimal, i.e., no smaller convex sublattice exists. Although the abstraction may introduce over-approximation, it has been proven to be conservative with respect to reachability of states.
Then, an unfolding semantics for Parametric Regulatory Networks is defined, taking advantage of concurrency between transitions to provide a compact representation of reachable transitions. A prototype implementation is provided: it has been applied to several examples of Boolean and multi-valued networks, showing its tractability for networks with numerous components.
△ Less
Submitted 16 March, 2018;
originally announced March 2018.
-
Goal-Driven Unfolding of Petri Nets
Authors:
Thomas Chatain,
Loïc Paulevé
Abstract:
Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for…
▽ More
Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.
△ Less
Submitted 4 November, 2016;
originally announced November 2016.
-
Relationship between the Reprogramming Determinants of Boolean Networks and their Interaction Graph
Authors:
Hugues Mandon,
Stefan Haar,
Loïc Paulevé
Abstract:
In this paper, we address the formal characterization of targets triggering cellular trans-differentiation in the scope of Boolean networks with asynchronous dynamics. Given two fixed points of a Boolean network, we are interested in all the combinations of mutations which allow to switch from one fixed point to the other, either possibly, or inevitably. In the case of existential reachability, we…
▽ More
In this paper, we address the formal characterization of targets triggering cellular trans-differentiation in the scope of Boolean networks with asynchronous dynamics. Given two fixed points of a Boolean network, we are interested in all the combinations of mutations which allow to switch from one fixed point to the other, either possibly, or inevitably. In the case of existential reachability, we prove that the set of nodes to (permanently) flip are only and necessarily in certain connected components of the interaction graph. In the case of inevitable reachability, we provide an algorithm to identify a subset of possible solutions.
△ Less
Submitted 19 August, 2016;
originally announced August 2016.
-
Goal-Oriented Reduction of Automata Networks
Authors:
Loïc Paulevé
Abstract:
We consider networks of finite-state machines having local transitions conditioned by the current state of other automata. In this paper, we depict a reduction procedure tailored for a given reachability property of the form ``from global state s there exists a sequence of transitions leading to a state where an automaton g is in a local state T'. By exploiting a causality analysis of the transiti…
▽ More
We consider networks of finite-state machines having local transitions conditioned by the current state of other automata. In this paper, we depict a reduction procedure tailored for a given reachability property of the form ``from global state s there exists a sequence of transitions leading to a state where an automaton g is in a local state T'. By exploiting a causality analysis of the transitions within the individual automata, the proposed reduction removes local transitions while preserving all the minimal traces that satisfy the reachability property. The complexity of the procedure is polynomial in the total number of local states and transitions, and exponential in the number of local states within one automaton. Applied to automata networks modelling dynamics of biological systems, we observe that the reduction shrinks down significantly the reachable state space, enhancing the tractability of the model-checking of large networks.
△ Less
Submitted 19 August, 2016;
originally announced August 2016.
-
Under-approximating Cut Sets for Reachability in Large Scale Automata Networks
Authors:
Loïc Paulevé,
Geoffroy Andrieux,
Heinz Koeppl
Abstract:
In the scope of discrete finite-state models of interacting components, we present a novel algorithm for identifying sets of local states of components whose activity is necessary for the reachability of a given local state. If all the local states from such a set are disabled in the model, the concerned reachability is impossible. Those sets are referred to as cut sets and are computed from a par…
▽ More
In the scope of discrete finite-state models of interacting components, we present a novel algorithm for identifying sets of local states of components whose activity is necessary for the reachability of a given local state. If all the local states from such a set are disabled in the model, the concerned reachability is impossible. Those sets are referred to as cut sets and are computed from a particular abstract causality structure, so-called Graph of Local Causality, inspired from previous work and generalised here to finite automata networks. The extracted sets of local states form an under-approximation of the complete minimal cut sets of the dynamics: there may exist smaller or additional cut sets for the given reachability. Applied to qualitative models of biological systems, such cut sets provide potential therapeutic targets that are proven to prevent molecules of interest to become active, up to the correctness of the model. Our new method makes tractable the formal analysis of very large scale networks, as illustrated by the computation of cut sets within a Boolean model of biological pathways interactions gathering more than 9000 components.
△ Less
Submitted 14 February, 2013;
originally announced February 2013.
-
Dynamical Properties of Discrete Reaction Networks
Authors:
Loïc Paulevé,
Gheorghe Craciun,
Heinz Koeppl
Abstract:
Reaction networks are commonly used to model the evolution of populations of species subject to transformations following an imposed stoichiometry. This paper focuses on the efficient characterisation of dynamical properties of Discrete Reaction Networks (DRNs). DRNs can be seen as modelling the underlying discrete nondeterministic transitions of stochastic models of reactions networks. In that se…
▽ More
Reaction networks are commonly used to model the evolution of populations of species subject to transformations following an imposed stoichiometry. This paper focuses on the efficient characterisation of dynamical properties of Discrete Reaction Networks (DRNs). DRNs can be seen as modelling the underlying discrete nondeterministic transitions of stochastic models of reactions networks. In that sense, any proof of non-reachability in DRNs directly applies to any concrete stochastic models, independently of kinetics laws and constants. Moreover, if stochastic kinetic rates never vanish, reachability properties are equivalent in the two settings. The analysis of two global dynamical properties of DRNs is addressed: irreducibility, i.e., the ability to reach any discrete state from any other state; and recurrence, i.e., the ability to return to any initial state. Our results consider both the verification of such properties when species are present in a large copy number, and in the general case. The obtained necessary and sufficient conditions involve algebraic conditions on the network reactions which in most cases can be verified using linear programming. Finally, the relationship of DRN irreducibility and recurrence with dynamical properties of stochastic and continuous models of reaction networks is discussed.
△ Less
Submitted 14 February, 2013;
originally announced February 2013.
-
Stochastic Simulation of Process Calculi for Biology
Authors:
Andrew Phillips,
Matthew Lakin,
Loïc Paulevé
Abstract:
Biological systems typically involve large numbers of components with complex, highly parallel interactions and intrinsic stochasticity. To model this complexity, numerous programming languages based on process calculi have been developed, many of which are expressive enough to generate unbounded numbers of molecular species and reactions. As a result of this expressiveness, such calculi cannot re…
▽ More
Biological systems typically involve large numbers of components with complex, highly parallel interactions and intrinsic stochasticity. To model this complexity, numerous programming languages based on process calculi have been developed, many of which are expressive enough to generate unbounded numbers of molecular species and reactions. As a result of this expressiveness, such calculi cannot rely on standard reaction-based simulation methods, which require fixed numbers of species and reactions. Rather than implementing custom stochastic simulation algorithms for each process calculus, we propose to use a generic abstract machine that can be instantiated to a range of process calculi and a range of reaction-based simulation algorithms. The abstract machine functions as a just-in-time compiler, which dynamically updates the set of possible reactions and chooses the next reaction in an iterative cycle. In this short paper we give a brief summary of the generic abstract machine, and show how it can be instantiated with the stochastic simulation algorithm known as Gillespie's Direct Method. We also discuss the wider implications of such an abstract machine, and outline how it can be used to simulate multiple calculi simultaneously within a common framework.
△ Less
Submitted 1 November, 2010;
originally announced November 2010.
