Continuous Petri Nets Faithfully Fluidify Most Permissive Boolean Networks

TL;DR

The paper addresses the gap between discrete MPBN dynamics and continuous refinements by fluidifying MPBNs with Continuous Petri nets (CPNs). It shows that the existing Boolean-network PN encoding, when instantiated as a CPN, faithfully simulates MP semantics, enabling the use of CPN symbolic analysis (ARG/SRT) to study MP attractors and long-term behaviour. The key result is a bidirectional reachability equivalence: MP reachability $\mathbf{x} \overset{mp}{\longrightarrow^*} \mathbf{y}$ corresponds to lim-reachability in the CPN encoding, $\langle \mathbf{y} \rangle \in \lim\!\mathbf{RS}_{\mathit{N}(f)}(\langle \mathbf{x} \rangle)$. This approach leverages polynomial CPN reachability and rich symbolic tools to analyze MPBNs, offering a principled bridge across the discrete-continuous abstraction scale with practical implications for studying attractors and pathway reasoning.

Abstract

The analysis of biological networks has benefited from the richness of Boolean networks (BNs) and the associated theory. These results have been further fortified in recent years by the emergence of Most Permissive (MP) semantics, combining efficient analysis methods with a greater capacity of explaining pathways to states hitherto thought unreachable, owing to limitations of the classical update modes. While MPBNs are understood to capture any behaviours that can be observed at a lower level of abstraction, all the way down to continuous refinements, the specifics and potential of the models and analysis, especially attractors, across the abstraction scale remain unexplored. Here, we fluidify MPBNs by means of Continuous Petri nets (CPNs), a model of (uncountably infinite) dynamic systems that has been successfully explored for modelling and theoretical purposes. CPNs create a formal link between MPBNs and their continuous dynamical refinements such as ODE models. The benefits of CPNs extend beyond the model refinement, and constitute well established theory and analysis methods, recently augmented by abstract and symbolic reachability graphs. These structures are shown to compact the possible behaviours of the system with focus on events which drive the choice of long-term behaviour in which the system eventually stabilises. The current paper brings an important keystone to this novel methodology for biological networks, namely the proof that extant PN encoding of BNs instantiated as a CPN simulates the MP semantics. In spite of the underlying dynamics being continuous, the analysis remains in the realm of discrete methods, constituting an extension of all previous work.

Figures (7)

• Figure 1: A running example BN on three variables (left) with its interaction graph (right). Positive interactions are depicted by pointed green arrows while negative interactions are depicted by flat red arrows.
• Figure 2: All configurations of the example BN (Figure \ref{['fig:running_example']}) reachable from $(0,0,0)$ under fully asynchronous semantics (left) and asynchronous semantics (right). The variables are ordered from top to bottom and dark tiles represent value $0$ while light tiles represent value $1$. Self-loops are omitted.
• Figure 3: All Boolean configurations of the example BN (Figure \ref{['fig:running_example']}) reachable from $(0,0,0)$ under MP semantics. While the fixed points are preserved, all other configurations become transiently reachable, as opposed to asynchronous semantics.
• Figure 4: Left: An example net with two places (depicted as circles) and two transitions (depicted as squares). The arc weights are given as labels on the arrows. As per convention, arc weights equal to $1$ are omitted. Right: An example of a transition firing in a DPN with the same net structure. The tokens assigned by the markings are depicted as black dots inside the places.
• Figure 5: The ARG (left) and the SRT (right) of the example net from Figure \ref{['fig:re_pn']}. The border edges are given as double line arrows in the ARG. The SRT for this example is trivial, as there is only one border edge.

Theorems & Definitions (12)

• definition 1: Petri Net Encoding of Boolean Networks
• lemma 1
• proof
• lemma 2
• proof
• lemma 3
• proof
• lemma 4
• proof
• corollary 1