Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks

要約

最小トラップ スペース (MTS) は、更新モードに関係なく、ブール ダイナミクスがトラップされるサブスペースをキャプチャします。
これらは、最も許容的なモードのアトラクターに対応します。
その多用途性により、MTS の計算は、基本的にその列挙に重点を置くことによって、最近注目を集めています。
この論文では、MTS のユニバーサル プロパティに関する論理的推論を 2 つの問題の範囲で扱います。1 つは、すべての MTS に特定のプロパティを強制するブール変数の永続的なフリーズを特定するためのブール ネットワークの再プログラミング、もう 1 つは MTS のユニバーサル プロパティからのブール ネットワークの合成です。
どちらの問題も、3 レベルの量指定子 ($\exists\forall\exists$) を使用して量化された命題論理式の充足可能性を解くことに帰着します。
この論文では、2 つの単純な式の解決を組み合わせることでこれらの問題を効率的に解決する反例ガイド付き洗練抽象化 (CEGAR) を紹介します。
私たちは、各式に対して Answer-Set プログラミングに依存するプロトタイプを提供し、生物学的ネットワークの幅広いブール モデルでの扱いやすさを示します。

要約(オリジナル)

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, Google