探究布尔网络最小陷阱空间的通用性质
Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks
AI总结：
本文针对布尔网络最小陷阱空间通用性质的两个推理问题，提出基于CEGAR的高效求解方法，通过耦合两个简单公式的求解实现，并用回答集编程实现原型，在生物网络模型上验证了可行性。
摘要：
最小陷阱空间（Minimal Trap Spaces, MTSs）刻画了无论更新模式如何，布尔动力学都会陷入其中的子空间，它们对应于最宽松模式的吸引子。由于其通用性，MTS的计算近年来受到关注，研究主要聚焦于其枚举问题。本文针对MTS通用性质的逻辑推理，研究了两个问题：一是布尔网络重编程，即识别能使所有MTS都满足给定性质的布尔变量永久冻结方式；二是从MTS的通用性质出发综合布尔网络。这两个问题都可归结为求解含三级量词（∃∀∃）的量化命题逻辑公式的可满足性。本文提出了一种反例引导的抽象精化（Counter-Example Guided Refinement Abstraction, CEGAR）方法，通过耦合两个更简单公式的求解来高效解决这些问题。我们基于回答集编程（Answer-Set Programming）为每个公式实现了原型系统，并在多种生物网络布尔模型上验证了该方法的可行性。
英文摘要：
Minimal trap spaces (MTSs) capture subspaces in which the Boolean dynamics is trapped, whatever the update mode. They correspond to the attractors of the most permissive mode. Due to their versatility, the computation of MTSs has recently gained traction, essentially by focusing on their enumeration. In this paper, we address the logical reasoning on universal properties of MTSs in the scope of two problems: the reprogramming of Boolean networks for identifying the permanent freeze of Boolean variables that enforce a given property on all the MTSs, and the synthesis of Boolean networks from universal properties on their MTSs. Both problems reduce to solving the satisfiability of quantified propositional logic formula with 3 levels of quantifiers ($\exists\forall\exists$). In this paper, we introduce a Counter-Example Guided Refinement Abstraction (CEGAR) to efficiently solve these problems by coupling the resolution of two simpler formulas. We provide a prototype relying on Answer-Set Programming for each formula and show its tractability on a wide range of Boolean models of biological networks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
