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.

翻译：生化系统同时涉及物质流（实体通过反应相互转化）和信息流（实体调控哪些反应可以发生）。布尔网络捕捉后者，反应网络捕捉前者。然而，尽管在系统生物学图形符号过程描述（SBGN-PD）语言等标准中，受调控的反应作为核心研究对象占据显著地位，但目前尚无统一的定性形式化方法将其作为主要研究目标。我们引入调制-反应网络（MR-网络）这一数学框架：在该框架中，实体通过激活和抑制作用调制反应，并研究其同步布尔语义。为推理MR-网络，我们发展了调制-反应逻辑（MRL）——一种混合模态$μ$-演算，其模态算子用于推理网络结构，不动点算子则刻画计算的时间演化。我们建立了一系列有效性质，包括单步更新规则的完整刻画，并通过形式化可达性、持续生产及吸引子存在性等生物学关注的特性，展示了MRL的表达能力。我们证明MRL可通过评估博弈实现模型检测，并引入MR-网络的互模拟关系，该关系被证明对所有MRL-公式保持不变。作为迈向更生物真实计算模型的一步，我们勾勒了MR-网络的异步语义，并概述了同步情况下的研究成果如何迁移到异步研究。