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.

翻译：最小陷阱空间（MTSs）捕捉了无论更新模式如何，布尔动力学都会陷入其中的子空间。它们对应于最许可模式下的吸引子。由于其通用性，MTS的计算近年来逐渐受到关注，主要集中在它们的枚举问题上。本文针对MTS普适性质的逻辑推理问题，探讨了两个方向：布尔网络重编程——通过识别布尔变量的永久冻结，使得所有MTS满足给定性质；以及基于MTS普适性质的布尔网络合成。这两个问题均可归约为求解具有三层量词($\exists\forall\exists$)的量化命题逻辑公式的可满足性。本文提出了一种反例引导的抽象精化（CEGAR）方法，通过耦合两个较简单公式的求解来高效处理这些问题。我们基于回答集编程为每个公式构建了原型系统，并在广泛的生物网络布尔模型上验证了其可处理性。