arxiv: 2604.03029 · v1 · submitted 2026-04-03 · 💻 cs.DM

Recognition: no theorem link

A Boolean encoding of the Most Permissive semantics for Boolean networks

Aur\'elien Naldi, Brigitte Moss\'e, \'Elisabeth Remy, Laure de Chancel

Pith reviewed 2026-05-13 18:25 UTC · model grok-4.3

classification 💻 cs.DM

keywords Boolean networksMost Permissive semanticsBoolean encodingasynchronous dynamicsattainabilitytriplet variablespartial unfolding

0 comments

The pith

Each component of a Boolean network is encoded as three Boolean variables whose asynchronous updates exactly reproduce Most Permissive attainability.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to embed the Most Permissive semantics of Boolean networks inside ordinary Boolean networks. Each original component is replaced by a triplet of Boolean variables that track distinct activity levels. New logical functions are derived for these variables so that the reachable states of the encoded network under asynchronous updates match precisely the states attainable in the original network under Most Permissive rules. The construction is realized as a modifier inside bioLQM and extended with optional partial unfolding to handle larger models.

Core claim

Representing each component by a triplet of Boolean variables and deriving the corresponding extended logical functions produces an asynchronous state graph whose reachable configurations are exactly the attainable states of the original network under Most Permissive semantics.

What carries the argument

The triplet representation of each component together with the derived logical functions that govern transitions among the three variables.

Load-bearing premise

The three Boolean variables and their update rules capture every intermediate activity level and transition allowed by Most Permissive semantics without adding or losing reachable states.

What would settle it

A concrete Boolean network and initial state for which some configuration reachable under Most Permissive semantics is unreachable in the asynchronous dynamics of the triplet-encoded network.

Figures

Figures reproduced from arXiv: 2604.03029 by Aur\'elien Naldi, Brigitte Moss\'e, \'Elisabeth Remy, Laure de Chancel.

**Figure 2.** Figure 2: State transition graphs from configuration [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

**Figure 3.** Figure 3: Left: Schema of transitions between levels for a Boolean variable. Right: Schema of transitions between levels for a variable [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗

**Figure 4.** Figure 4: STG from initial configuration 111 for Example A in Most Permissive semantics. Only Boolean configurations are shown. Configurations in red are those reachable with Most Permissive semantics, but not with classical semantics. Solid arrows represent transitions that are possible with classical semantics, while dotted arrows are those that pass through the increasing or decreasing level of Most Permissive. 1… view at source ↗

**Figure 5.** Figure 5: Encoding with three Boolean variables of the Most Permissive semantics. Green and red edges represent controlled transitions, [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗

**Figure 6.** Figure 6: Regulatory graph associated with the extended Example A. Red arrows represent negative regulations, green arrows positive [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗

**Figure 7.** Figure 7: Regulatory graph of Example B. However, it may be desirable to unfold only a subset of the components. Chosen components are transformed into triplets with associated internal rules. The extended components are integrated into the network through their internal control functions, as described in Section 2.2.2. The use of the partial unfolding implies knowing which components are worth extending. This parti… view at source ↗

**Figure 8.** Figure 8: Regulatory graph associated with the model B extended for Fli1. [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗

**Figure 5.** Figure 5: The character X indicates values that depend actually on the index [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗

**Figure 9.** Figure 9: Guaranteed internal regulations between xja, xjb and xjc. Green arrows represent positive regulations. Blue arrows represent regulations with undetermined sign. Three other regulations may occur, not already seen above as guaranteed internal regulations, and that are depending on conditions. • Inhibition of xjc by xjb: Given j ∈ {1, . . . , n} and a configuration x ∈ B 3n whose jth triplet is equal to 000,… view at source ↗

read the original abstract

Boolean networks are widely used to model biological regulatory networks and study their dynamics. Classical semantics, such as the asynchronous semantics, do not always accurately capture transient or asymptotic behaviors observed in quantitative models. To address this limitation, the Most Permissive semantics was introduced by Paulev\'e et al., extending Boolean dynamics with intermediate activity levels that allow components to transiently activate or inhibit their targets during transitions. In this work, we provide a Boolean encoding of the Most Permissive semantics: each component of the original network is represented by a triplet of Boolean variables, and we derive the extended logical function governing the resulting network. We prove that the asynchronous dynamics of the encoded network exactly reproduces the attainability properties of the original network under Most Permissive semantics. This encoding is implemented as a modifier within the bioLQM framework, making it directly compatible with existing tools such as GINsim. To address scalability limitations, we further extend the tool to support partial unfolding, restricted to a user-defined subset of components.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The triplet encoding gives a workable Boolean way to run Most Permissive attainability inside ordinary asynchronous updates, with a proof and a bioLQM implementation.

read the letter

The main thing to know is that this paper supplies a triplet encoding for each component and proves that the asynchronous dynamics of the new network match the attainability properties of the original under Most Permissive semantics. That equivalence is the central result, and the authors ship it as a modifier in bioLQM so it runs inside GINsim without new infrastructure. Partial unfolding restricted to user-chosen components is included to keep state spaces manageable on larger models. The construction itself is new relative to the encodings cited in the abstract, and the implementation focus makes the work immediately usable for people already running Boolean network tools. The paper handles the practical side cleanly by staying compatible with existing frameworks rather than requiring a separate simulator. On the soft spots, the stress-test point about non-monotonic regulations is worth checking in the derivation. If the triplet update rules introduce any ordering assumption or miss certain transient inhibitions or activations allowed by arbitrary regulatory functions, some attainability paths could shift. The abstract presents the proof as general, so the full details should show whether it holds without monotonicity restrictions. The partial unfolding is a reasonable engineering choice but the paper does not appear to include quantitative benchmarks on how much it reduces the state space in practice. This is aimed at computational biologists and discrete modelers who already use Boolean networks and want to test Most Permissive behaviors on their current setups. A reader working on regulatory dynamics will get direct value from the encoding and the tool hook. It deserves a serious referee because the equivalence claim is non-trivial and the implementation lets others verify the result on their own models. I would send it out for review.

Referee Report

1 major / 1 minor

Summary. The paper claims to provide a Boolean encoding of the Most Permissive semantics for Boolean networks. Each original component is represented by a triplet of Boolean variables, from which extended logical functions are derived for an encoded network. The central result is a proof that the asynchronous dynamics of this encoded network exactly reproduce the attainability properties of the original network under Most Permissive semantics. The encoding is implemented as a modifier in the bioLQM framework (compatible with GINsim) and extended with partial unfolding for selected components to address scalability.

Significance. If the equivalence holds, the encoding would enable direct use of existing Boolean-network tools and algorithms to compute Most Permissive reachability and attractors, without re-implementing the permissive semantics. This is practically useful for biological modeling where transient intermediate levels matter, and the bioLQM integration plus partial-unfolding option lowers the barrier to adoption.

major comments (1)

[Construction of the logical functions for the triplet variables] The proof that the derived update functions for the three Boolean variables per component preserve exactly the Most Permissive attainability relations (abstract and main construction) must be checked for non-monotonic regulatory functions. The triplet representation and logical-function derivation may implicitly rely on a fixed ordering of activity levels; for a non-monotonic target function the intermediate transitions allowed under Most Permissive semantics could become unreachable or new spurious paths could appear after projection back to the original components. An explicit general argument or a set of non-monotonic test cases with full state-space enumeration is required.

minor comments (1)

[Abstract] The abstract states that a proof is given but does not cite the theorem number or section containing the formal statement and proof of equivalence.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation of the significance of our contribution and for the detailed comment on the logical-function construction. We address the concern point by point below.

read point-by-point responses

Referee: [Construction of the logical functions for the triplet variables] The proof that the derived update functions for the three Boolean variables per component preserve exactly the Most Permissive attainability relations (abstract and main construction) must be checked for non-monotonic regulatory functions. The triplet representation and logical-function derivation may implicitly rely on a fixed ordering of activity levels; for a non-monotonic target function the intermediate transitions allowed under Most Permissive semantics could become unreachable or new spurious paths could appear after projection back to the original components. An explicit general argument or a set of non-monotonic test cases with full state-space enumeration is required.

Authors: The proof and construction are formulated for arbitrary Boolean functions and do not rely on monotonicity. The triplet variables encode the three activity levels (0, 1, 2) permitted under Most Permissive semantics, and the update functions are obtained by determining, for every combination of input levels, the possible output levels that the original function can produce under the Most Permissive rules. These rules are defined directly from the Boolean function without any monotonicity hypothesis; the ordering 0 < 1 < 2 is part of the semantics itself and does not restrict the set of admissible transitions for non-monotonic targets. Consequently, no spurious paths are introduced and no valid Most Permissive transitions are lost upon projection. To make this explicit, the revised manuscript adds a clarifying paragraph immediately after the main theorem stating that the argument holds for any Boolean function, together with an appendix containing two fully enumerated non-monotonic examples (a single-component non-monotonic function and a two-component network containing a non-monotonic regulator) that confirm exact agreement between the encoded asynchronous dynamics and the Most Permissive attainability relation. revision: yes

Circularity Check

0 steps flagged

Encoding and proof are self-contained; no reduction to inputs or self-citations

full rationale

The paper defines a triplet encoding for each component, derives the extended logical functions from the original regulatory functions, and proves equivalence of asynchronous dynamics to Most Permissive attainability properties. This is a direct constructive mapping and proof rather than any fitted parameter, self-definitional loop, or load-bearing self-citation. The cited Most Permissive semantics originates from independent prior work (Paulevé et al.), and the central claim does not reduce by construction to its own inputs or prior author results. The derivation stands as independent content against the stated semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard Boolean logic and asynchronous update rules plus the new triplet representation; no free parameters or ad-hoc axioms beyond domain-standard Boolean algebra are indicated in the abstract.

axioms (1)

standard math Standard Boolean algebra and asynchronous update semantics apply to the encoded network
Invoked to define the extended logical functions and dynamics.

invented entities (1)

Triplet of Boolean variables per original component no independent evidence
purpose: Represent intermediate activity levels under Most Permissive semantics
New representation introduced to encode the permissive transitions.

pith-pipeline@v0.9.0 · 5482 in / 1155 out tokens · 38654 ms · 2026-05-13T18:25:16.598870+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

9 extracted references · 9 canonical work pages

[1]

RefiningBooleanmodelswiththepartialmostpermissivescheme

NadineBenBoinaetal.“RefiningBooleanmodelswiththepartialmostpermissivescheme”.In:Bioinformatics 41.4 (Mar. 2025), btaf123.issn: 1367-4811.doi:10 . 1093 / bioinformatics / btaf123. eprint:https : / / academic.oup.com/bioinformatics/article-pdf/41/4/btaf123/62523863/btaf123.pdf.url:https: //doi.org/10.1093/bioinformatics/btaf123

work page doi:10.1093/bioinformatics/btaf123 2025
[2]

Logical Modelling of Gene Regulatory Networks with GINsim

Claudine Chaouiya, Aurélien Naldi, and Denis Thieffry. “Logical Modelling of Gene Regulatory Networks with GINsim.” In:Methods in molecular biology (Clifton, N.J.)Vol. 804. 2012 2012, pp. 463–79

work page 2012
[3]

SBML qualitative models: a model representation format and infrastructure to foster interactions between qualitative modelling formalisms and tools

Claudine Chaouiya et al. “SBML qualitative models: a model representation format and infrastructure to foster interactions between qualitative modelling formalisms and tools”. In:BMC Systems Biology. 2013

work page 2013
[4]

A novel Boolean network inference strategy to model early hematopoiesis aging

Léonard Hérault et al. “A novel Boolean network inference strategy to model early hematopoiesis aging”. In: bioRxiv(2022).doi:10.1101/2022.02.08.479548. eprint:https://www.biorxiv.org/content/early/ 2022/05/08/2022.02.08.479548.full.pdf.url:https://www.biorxiv.org/content/early/2022/05/ 08/2022.02.08.479548

work page doi:10.1101/2022.02.08.479548 2022
[6]

Réseaux booléens : méthodes formelles et outils pour la modélisation en biologie

Loïc Paulevé. “Réseaux booléens : méthodes formelles et outils pour la modélisation en biologie”. Habilitation à diriger des recherches. Université Paris-Saclay, Sept. 2020.url:https://tel.archives-ouvertes.fr/tel- 03150976

work page 2020
[7]

Reconciling Qualitative, Abstract, and Scalable Modeling of Biological Networks

Loïc Paulevé et al. “Reconciling Qualitative, Abstract, and Scalable Modeling of Biological Networks”. In: (Mar. 2020).doi:10.1101/2020.03.22.998377

work page doi:10.1101/2020.03.22.998377 2020
[8]

2022.doi: 10.48550/ARXIV.2206.12729.url:https://arxiv.org/abs/2206.12729

Théo Roncalli and Loïc Paulevé.Variable-Depth Simulation of Most Permissive Boolean Networks. 2022.doi: 10.48550/ARXIV.2206.12729.url:https://arxiv.org/abs/2206.12729

work page doi:10.48550/arxiv.2206.12729.url:https://arxiv.org/abs/2206.12729 2022
[9]

Continuous time Boolean modeling for biological signaling: application of Gillespie algo- rithm

Gautier Stoll et al. “Continuous time Boolean modeling for biological signaling: application of Gillespie algo- rithm.” In: (Aug. 2012).doi:10.1186/1752-0509-6-116

work page doi:10.1186/1752-0509-6-116 2012
[10]

Boolean formalization of genetic control circuits

René Thomas. “Boolean formalization of genetic control circuits”. In:Journal of Theoretical Biology42.3 (1973), pp. 563–585.issn: 0022-5193.doi:https : / / doi . org / 10 . 1016 / 0022 - 5193(73 ) 90247 - 6.url: https://www.sciencedirect.com/science/article/pii/0022519373902476. 12 APPENDIX 0 - The Most Permissive dynamics of Example A We give the list of...

work page arXiv 1973