pith. sign in

arxiv: 2606.01193 · v1 · pith:CIJYOBAYnew · submitted 2026-05-31 · 💻 cs.LO · q-bio.MN· q-bio.QM

Modulation-Reaction Networks

Leo Lobski , Yo\`av Montacute This is my paper

Pith reviewed 2026-06-28 16:16 UTC · model grok-4.3

classification 💻 cs.LO q-bio.MNq-bio.QM
keywords modulation-reaction networksModulation-Reaction LogicBoolean semanticshybrid modal mu-calculusbiochemical regulationreachabilityattractorsbisimulation
0
0 comments X

The pith

Modulation-reaction networks treat regulated reactions as primary objects by letting entities activate or inhibit specific reactions, and Modulation-Reaction Logic reasons about their structure and dynamics.

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

The paper introduces modulation-reaction networks to unify the flow of matter through reactions with the flow of regulatory information through activations and inhibitions. It develops Modulation-Reaction Logic as a hybrid modal mu-calculus whose modalities address network structure and whose fixed-point operators address temporal change under synchronous Boolean semantics. The logic supplies a complete characterisation of the one-step update rule and expresses properties such as reachability, sustained production, and the presence of attractors, while also admitting model checking via evaluation games and a bisimulation that preserves all formulas.

Core claim

MR-networks model entities that modulate reactions via activations and inhibitions. Under synchronous Boolean semantics, Modulation-Reaction Logic provides a complete characterisation of the one-step update rule and formalises biological properties including reachability, sustained production, and attractors. Model checking proceeds through an evaluation game, and a bisimulation relation on MR-networks is invariant under every MRL formula.

What carries the argument

Modulation-reaction networks, in which entities modulate reactions through activations and inhibitions under synchronous Boolean semantics, together with the hybrid modal mu-calculus MRL whose modalities capture network structure and fixed points capture temporal evolution.

If this is right

  • Reachability of states, sustained production of entities, and presence of attractors can be formalised directly in MRL.
  • The one-step update rule receives a complete logical characterisation.
  • Model checking of MRL formulas on MR-networks is possible via an evaluation game.
  • A bisimulation relation on MR-networks preserves the truth of every MRL formula.
  • The framework and its developments extend in outline to an asynchronous semantics of MR-networks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The separation of reaction structure from regulatory modulation may allow modular verification when only the regulation changes.
  • The bisimulation could support reduction of large networks while preserving all expressible biological properties.
  • Transfer to asynchronous semantics may enable reasoning about timing-dependent regulation without moving to fully stochastic models.

Load-bearing premise

The synchronous Boolean semantics chosen for MR-networks adequately abstracts regulated biochemical dynamics and the hybrid modal mu-calculus modalities and fixed points are the right primitives for the intended structural and temporal properties.

What would settle it

A concrete MR-network in which the logical characterisation of the one-step update rule fails to match the actual synchronous update computed directly from the network definition, or a biological property such as attractor presence that is observable in the dynamics but cannot be expressed by any MRL formula.

Figures

Figures reproduced from arXiv: 2606.01193 by Leo Lobski, Yo\`av Montacute.

Figure 1
Figure 1. Figure 1: A: An example of a regulatory graph taken from [10, [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: An example of an SBGN-PD diagram with one process and one modulation, taken from [19, [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: An encoding of an MR-network as a Boolean network. Translation to Boolean networks. Every MR-network can be encoded as a regula￾tory graph with the same vertices and three binary relations: reaction, activation and inhibition relations, as well as a label for each edge in the graph. We give an example translation from an MR-network to the corresponding regulatory graph in [PITH_FULL_IMAGE:figures/full_fig… view at source ↗
Figure 4
Figure 4. Figure 4: An open MR-network with labels. Consider the open MR-network with labels in [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: An example computation of an open labelled MR-network. properties in MRL with respect to the synchronous semantics. Our usage of the fixed-point modalities streamlines and unifies many properties studied in the literature on a case-by-case basis. While the synchronous update rule is inad￾equate for most biological applications, we believe that the modular approach taken here – separating networks, computat… view at source ↗
read the original abstract

Biochemical systems involve both the flow of matter, in which entities transform into one another via reactions, and the flow of information, in which entities regulate which reactions may occur. Boolean networks capture the latter; reaction networks capture the former. Yet no unified qualitative formalism treats regulated reactions as its principal objects of study, despite their prominence in standards such as the Systems Biology Graphical Notation Process Description (SBGN-PD) language. We introduce modulation-reaction networks (MR-networks), a mathematical framework in which entities modulate reactions through activations and inhibitions, and study their synchronous Boolean semantics. To reason about MR-networks we develop Modulation-Reaction Logic (MRL), a hybrid modal $\mu$-calculus whose modalities reason about the structure of the network and whose fixed-point operators capture temporal evolution of the computation. We establish a collection of validities, including a complete characterisation of the one-step update rule, and demonstrate the expressive power of MRL by formalising properties of biological interest such as reachability, sustained production, and presence of attractors. We show that MRL admits model-checking via an evaluation game, and introduce a bisimulation relation for MR-networks, which is proved to be invariant for all MRL-formulas. As a step towards a biologically more realistic computational model, we sketch the asynchronous semantics of MR-networks, and outline how the developments for the synchronous case transfer to the study of the asynchronous one.

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.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces modulation-reaction networks (MR-networks) as a framework unifying reaction networks (matter flow) and regulatory activations/inhibitions (information flow). It equips MR-networks with synchronous Boolean update semantics, develops Modulation-Reaction Logic (MRL) as a hybrid modal μ-calculus whose modalities capture network structure and whose fixed points capture temporal evolution, claims a collection of validities including a complete characterisation of the one-step update rule, demonstrates MRL's expressive power by encoding biological properties such as reachability, sustained production and attractors, supplies an evaluation-game model-checking procedure, proves bisimulation invariance for MRL, and sketches an asynchronous semantics together with a transfer argument for the synchronous results.

Significance. If the technical claims hold, the work supplies a qualitative formalism directly aligned with SBGN-PD Process Description diagrams and therefore fills a genuine gap between Boolean networks and reaction networks. The hybrid modal μ-calculus approach, game semantics, and bisimulation result are standard strengths that would make the logic immediately usable for automated verification. The explicit sketch of asynchronous semantics is a constructive step toward biological realism. The absence of any concrete biological example, comparison with SBML/ODE models, or parameter-free derivation, however, keeps the practical significance modest at present.

major comments (2)
  1. [Abstract] Abstract (asynchronous semantics paragraph): the statement that 'the developments for the synchronous case transfer to the study of the asynchronous one' is load-bearing for any claim of improved biological realism, yet the visible text supplies neither a formal definition of the asynchronous update rule nor a proof that the complete characterisation of the one-step update rule, the MRL validities, or bisimulation invariance survive the change from synchronous to asynchronous semantics.
  2. [Abstract] Abstract (MRL expressive-power paragraph): the claim that MRL can formalise 'reachability, sustained production, and presence of attractors' is central to the biological motivation, but no MRL formulas, no encoding of the one-step update rule, and no example network are exhibited, so it is impossible to verify that the hybrid modalities and fixed-point operators are adequate for these properties.
minor comments (2)
  1. The abstract refers to 'a collection of validities' without enumerating them beyond the update-rule characterisation; a short list or reference to the relevant theorem would improve readability.
  2. No comparison is drawn with existing qualitative frameworks (e.g., Boolean regulatory networks or Petri-net encodings of SBGN-PD), which would help situate the novelty of MR-networks.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. The two major comments both concern the abstract's condensation of technical claims whose supporting material appears in the body of the manuscript. We respond point by point and indicate the revisions we will undertake.

read point-by-point responses

  1. Referee: [Abstract] Abstract (asynchronous semantics paragraph): the statement that 'the developments for the synchronous case transfer to the study of the asynchronous one' is load-bearing for any claim of improved biological realism, yet the visible text supplies neither a formal definition of the asynchronous update rule nor a proof that the complete characterisation of the one-step update rule, the MRL validities, or bisimulation invariance survive the change from synchronous to asynchronous semantics.

    Authors: Section 5 of the manuscript already sketches an asynchronous update rule and outlines a transfer argument for the synchronous results. We agree, however, that the abstract claim is insufficiently supported without a self-contained formal statement and proof. In the revision we will expand Section 5 to give an explicit definition of the asynchronous semantics and a detailed (if concise) argument showing that the one-step characterisation, the listed validities, and bisimulation invariance all carry over. The abstract will be updated to reflect the strengthened treatment. revision: yes

  2. Referee: [Abstract] Abstract (MRL expressive-power paragraph): the claim that MRL can formalise 'reachability, sustained production, and presence of attractors' is central to the biological motivation, but no MRL formulas, no encoding of the one-step update rule, and no example network are exhibited, so it is impossible to verify that the hybrid modalities and fixed-point operators are adequate for these properties.

    Authors: The body of the paper (Section 4) supplies explicit MRL formulas for reachability, sustained production and attractors, together with an encoding of the one-step update rule, all illustrated on a small concrete MR-network. The abstract summarises these results without reproducing the formulas. To address the referee's concern we will insert a short illustrative example (one network plus the corresponding MRL formulas) either into a revised abstract or into a new early subsection, making the encodings immediately visible. revision: yes

Circularity Check

0 steps flagged

No circularity; framework definitions and logic are self-contained.

full rationale

The paper introduces MR-networks and MRL as new definitions, then states that it establishes validities (including characterisation of the update rule) and demonstrates expressive power via formalisation of properties. No equations, fitted parameters, or self-citation chains are quoted that reduce any claimed result to its own inputs by construction. The synchronous Boolean semantics is presented as a chosen abstraction rather than derived, and the transfer to asynchronous case is sketched without load-bearing self-referential steps. This is a standard definitional contribution with independent content.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no visible free parameters, axioms, or invented entities beyond the introduction of the new network class and logic itself.

pith-pipeline@v0.9.1-grok · 5786 in / 1194 out tokens · 30999 ms · 2026-06-28T16:16:52.354613+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 20 canonical work pages

  1. [1]

    Compositionality6(2024)

    Aduddell, R., Fairbanks, J., Kumar, A., Ocal, P.S., Patterson, E., Shapiro, B.T.: A compositional account of motifs, mechanisms, and dynamics in biochemi- cal regulatory networks. Compositionality6(2024). https://doi.org/10.32408/ compositionality-6-2

    2024

  2. [2]

    IEEE/ACM Trans

    Andersen, J.L., Flamm, C., Merkle, D., Stadler, P.F.: Chemical transformation motifs – modelling pathways as integer hyperflows. IEEE/ACM Trans. Comput. Biol. Bioinformatics16(2), 510–523 (2019). https://doi.org/10.1109/TCBB.2017. 2781724

    work page doi:10.1109/tcbb.2017 2019

  3. [3]

    In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F

    Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, pp. 821–868. Studies in logic and prac- tical reasoning, North-Holland (2007). https://doi.org/10.1016/S1570-2464(07) 80017-6

    work page doi:10.1016/s1570-2464(07 2007

  4. [4]

    Bonchi, F., Sobociński, P., Zanasi, F.: A Survey of Compositional Signal Flow Theory, pp. 29–56. Springer International Publishing, Cham (2021). https://doi. org/10.1007/978-3-030-81701-5_2

    work page doi:10.1007/978-3-030-81701-5_2 2021

  5. [5]

    Journal of The Royal Society Interface5(suppl_1), S85–S94 (2008)

    Bornholdt, S.: Boolean network models of cellular regulation: prospects and lim- itations. Journal of The Royal Society Interface5(suppl_1), S85–S94 (2008). https://doi.org/10.1098/rsif.2008.0132.focus

    work page doi:10.1098/rsif.2008.0132.focus 2008

  6. [6]

    Bioinformatics22(14), 1805–1807 (2006)

    Calzone, L., Fages, F., Soliman, S.: Biocham: an environment for modeling bio- logical systems and formalizing experimental knowledge. Bioinformatics22(14), 1805–1807 (2006). https://doi.org/10.1093/bioinformatics/btl172

    work page doi:10.1093/bioinformatics/btl172 2006

  7. [7]

    In: Danos, V., Schachter, V

    Chabrier-Rivier, N., Fages, F., Soliman, S.: The biochemical abstract machine biocham. In: Danos, V., Schachter, V. (eds.) Computational Methods in Sys- tems Biology. pp. 172–191. Springer Berlin Heidelberg, Berlin, Heidelberg (2005). https://doi.org/10.1007/978-3-540-25974-9_14

    work page doi:10.1007/978-3-540-25974-9_14 2005

  8. [8]

    In: Fages, F., Pérès, S

    Chaouiya, C., Feret, J., Tenera Roxo, P.: On model reductions of boolean net- works. In: Fages, F., Pérès, S. (eds.) Computational Methods in Systems Biology. pp. 42–60. Springer Nature Switzerland, Cham (2026). https://doi.org/10.1007/ 978-3-032-01436-8_3

    2026

  9. [9]

    https://doi.org/10.48550/arXiv.2410.18024

    Chaudhuri, A., Köhl, R., Wolkenhauer, O.: A mathematical framework to study organising principles in graphical representations of biochemical processes (2026). https://doi.org/10.48550/arXiv.2410.18024

    work page doi:10.48550/arxiv.2410.18024 2026

  10. [10]

    In: Fages, F., Pérès, S

    Cury, J.E.R., Tenera Roxo, P., Manquinho, V., Chaouiya, C., Monteiro, P.T.: Com- putation of immediate neighbours of monotone boolean functions. In: Fages, F., Pérès, S. (eds.) Computational Methods in Systems Biology. pp. 3–22. Springer Nature Switzerland (2026). https://doi.org/10.1007/978-3-032-01436-8_1

    work page doi:10.1007/978-3-032-01436-8_1 2026

  11. [11]

    IEEE/ACM Trans

    Fages, F., Martinez, T., Rosenblueth, D.A., Soliman, S.: Influence networks com- pared with reaction networks: Semantics, expressivity and attractors. IEEE/ACM Trans. Comput. Biol. Bioinformatics15(4), 1138–1151 (2018). https://doi.org/10. 1109/TCBB.2018.2805686

    arXiv 2018

  12. [12]

    Theoretical Computer Science599, 64–78 (2015)

    Fages, F., Gay, S., Soliman, S.: Inferring reaction systems from ordinary differential equations. Theoretical Computer Science599, 64–78 (2015). https://doi.org/10. 1016/j.tcs.2014.07.032, advances in Computational Methods in Systems Biology Modulation-Reaction Networks 19

    2015

  13. [13]

    Seeing the trees and their branches in the network is hard

    Fages, F., Soliman, S.: Abstract interpretation and types for systems biology. Theo- reticalComputerScience403(1),52–70(2008).https://doi.org/10.1016/j.tcs.2008. 04.024

    work page doi:10.1016/j.tcs.2008 2008

  14. [14]

    Journal of Theoretical Biology22(3), 437–467 (1969)

    Kauffman, S.: Metabolic stability and epigenesis in randomly constructed genetic nets. Journal of Theoretical Biology22(3), 437–467 (1969). https://doi.org/10. 1016/0022-5193(69)90015-0

    1969

  15. [15]

    In: Petre, I., Păun, A

    Niehren, J., Vaginay, A., Versari, C.: Abstract simulation of reaction networks via boolean networks. In: Petre, I., Păun, A. (eds.) Computational Methods in SystemsBiology.pp.21–40.SpringerInternationalPublishing,Cham(2022).https: //doi.org/10.1007/978-3-031-15034-0_2

    work page doi:10.1007/978-3-031-15034-0_2 2022

  16. [16]

    Mathematical Structures in Computer Sci- ence22(4), 651–685 (2012)

    Paulevé, L., Magnin, M., Roux, O.: Static analysis of biological regulatory networks dynamics using abstract interpretation. Mathematical Structures in Computer Sci- ence22(4), 651–685 (2012). https://doi.org/10.1017/S0960129511000739

    work page doi:10.1017/s0960129511000739 2012

  17. [17]

    Paulevé, L., Sené, S.: Boolean Networks and Their Dynamics: The Impact of Up- dates, chap. 6, pp. 173–250. John Wiley & Sons, Ltd (2022). https://doi.org/10. 1002/9781119716600.ch6

    2022

  18. [18]

    BMC systems biology10(1), 42– (2016)

    Rougny, A., Froidevaux, C., Calzone, L., Paulevé, L.: Qualitative dynamics se- mantics for sbgn process description. BMC systems biology10(1), 42– (2016). https://doi.org/10.1186/s12918-016-0285-0

    work page doi:10.1186/s12918-016-0285-0 2016

  19. [19]

    Journal of Integrative Bioinfor- matics16(2), 20190022 (2019)

    Rougny, A., Touré, V., Moodie, S., Balaur, I., Czauderna, T., Borlinghaus, H., Do- grusoz, U., Mazein, A., Dräger, A., Blinov, M.L., Villéger, A., Haw, R., Demir, E., Mi, H., Sorokin, A., Schreiber, F., Luna, A.: Systems biology graphical notation: Process description language level 1 version 2.0. Journal of Integrative Bioinfor- matics16(2), 20190022 (20...

    work page doi:10.1515/jib-2019-0022 2019

  20. [20]

    A Dynamic Recursive Unified Internet Design (DRUID),

    Rutten, J.J.: A tutorial on coinductive stream calculus and signal flow graphs. Theoretical Computer Science343(3), 443–481 (2005). https://doi.org/10.1016/j. tcs.2005.06.019, formal Methods for Components and Objects

    work page doi:10.1016/j 2005

  21. [21]

    In: Horecker, B.L., Stadtman, E.R

    Savageau, M.A.: The behavior of intact biochemical control systems. In: Horecker, B.L., Stadtman, E.R. (eds.) Current Topics in Cellular Regulation, vol. 6, pp. 63–

  22. [22]

    https://doi.org/10.1016/B978-0-12-152806-5.50010-2

    Academic Press (1972). https://doi.org/10.1016/B978-0-12-152806-5.50010-2

    work page doi:10.1016/b978-0-12-152806-5.50010-2 1972

  23. [23]

    Report to National Defense Research Council, January, 1942., pp

    Shannon, C.E.: The Theory and Design of Linear Differential Equation Machines. Report to National Defense Research Council, January, 1942., pp. 514–559. Wiley- IEEE Press (1942). https://doi.org/10.1109/9780470544242.ch33

    work page doi:10.1109/9780470544242.ch33 1942

  24. [24]

    Biosys- tems50(1), 49–59 (1999)

    Thieffry, D., Romero, D.: The modularity of biological regulatory networks. Biosys- tems50(1), 49–59 (1999). https://doi.org/10.1016/S0303-2647(98)00087-2

    work page doi:10.1016/s0303-2647(98)00087-2 1999

  25. [25]

    Journal of Theoreti- cal Biology42(3), 563–585 (1973)

    Thomas, R.: Boolean formalization of genetic control circuits. Journal of Theoreti- cal Biology42(3), 563–585 (1973). https://doi.org/10.1016/0022-5193(73)90247-6

    work page doi:10.1016/0022-5193(73)90247-6 1973

  26. [26]

    International Scholarly Research Notices2013(1), 897658 (2013)

    Voit, E.O.: Biochemical systems theory: A review. International Scholarly Research Notices2013(1), 897658 (2013). https://doi.org/10.1155/2013/897658

    work page doi:10.1155/2013/897658 2013

  27. [27]

    Physical Biology9(5), 055001 (2012)

    Wang, R.S., Saadatpour, A., Albert, R.: Boolean modeling in systems biology: an overview of methodology and applications. Physical Biology9(5), 055001 (2012). https://doi.org/10.1088/1478-3975/9/5/055001

    work page doi:10.1088/1478-3975/9/5/055001 2012