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.

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