Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks

要約

タイトル：ブールネットワークの最小トラップ空間の普遍的な特性に対処する
要約：
– 最小トラップ空間（MTS）は、アップデート方法に関係なく、ブールダイナミクスが閉じ込められる部分空間を捉えます。彼らは最も寛容なモードのアトラクタに対応します。
– 彼らの多様性のために、MTSの計算は最近注目され、主にその列挙に焦点が当てられています。
– この論文では、すべてのMTSに対して所望の特性を強制するブール変数の永久的な凍結を特定するためのブールネットワークの再プログラム、および、MTS上の普遍的な特性からブールネットワークを合成する問題の論理推論について、考察されています。
– 両方の問題は、3つの量化命題論理式の充足可能性を解決することに帰着されます（forall、exists、exists）。
– この論文では、2つのシンプルな式の解決をカップリングすることにより、これらの問題を効率的に解決するためのカウンターエキスパートガイドリファインメント抽象（CEGAR）を紹介します。
– 私たちは、それぞれの式に基づくアンサーセットプログラミングに依存したプロトタイプを提供し、生物学的ネットワークの広範なブールモデルでのトラクタビリティを示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI