Modulation-Reaction Networks
This work provides a novel mathematical framework for modeling regulated reactions in systems biology, addressing a gap between Boolean networks and reaction networks.
The authors introduce modulation-reaction networks (MR-networks), a unified qualitative formalism for biochemical systems that integrates both matter flow (reactions) and information flow (regulations). They develop Modulation-Reaction Logic (MRL) for reasoning about these networks, establish validities including a complete one-step update rule, and demonstrate model-checking via an evaluation game and a bisimulation relation.
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 $μ$-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.