Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation

技術要約：定量的離散近似による生化学的動的システムの到達可能性

問題提起
システム生物学は、基礎となる生化学から生じる創発的な振る舞いを調査するために、生物の実行可能なモデルを再構築することを目指している。常微分方程式（ODE）は、これらの生化学的動的システムをモデリングするための標準であるが、グローバルな解析においては重大な課題を提示する。具体的には、到達可能性問題（例：特定の初期条件に対して、振動や特定の濃度レベルといった動的な現象が発生するかどうかを判定すること）は、連続的な状態空間が非有界かつ非可算であるため、一般に決定不能である。

既存の解析手法は数値シミュレーションに依存することが多いが、これは単一の初期点からの「ローカル」な解析に限定される。グローバルな解析を実現するために、研究者は長方形抽象化などの有限の離散近似を用いる。しかし、従来の長方形抽象化技術は、高いレベルの「偽の振る舞い（spurious behavior）」に苦しむ。これらの手法は、境界（ファセット）におけるベクトル場を過剰近似するものの、軌道の具体的な履歴を追跡しないため、実際の連続システムには存在しない状態遷移を多数生成してしまう。分割密度を高めても、この問題を効果的に排除できるとは限らない。

手法
著者らは、特にマルチアフィン・ベクトル場（各変数に対してアフィン）によってモデル化される生化学的システムを対象とした、連続動的システムの有限離散近似のための新しい計算手法を提案している。その核となるのが、**定量的離散近似オートマトン（QDAA）**である。

1. 状態の定義： 標準的な長方形抽象化では、状態は単なる長方形として定義されるが、QDAAにおける状態は、長方形 $H$（分割された状態空間内のセル）と「進入集合（entry set）」$E$ のペア $\langle H, E \rangle$ として定義される。進入集合 $E$ は、$H$ の特定のファセットの部分集合であり、軌道が長方形に進入する経路を表す。この局所的なメモリは、システムの進化の履歴を符号化する。
2. 焦点部分集合による定量化： 各状態 $\langle H, E \rangle$ に対して、手法は「焦点部分集合（focal subsets）」を特定する。これらは、すべての軌道が特定の出口ファセットに向かう（あるいは長方形内に留まり続ける）進入集合の部分集合である。
3. 重み付き遷移： 状態間の遷移には、焦点部分集合の相対的な体積（ルベーグ測度）に基づいて重みが割り当てられる。具体的には、状態 $A$ から $B$ への遷移の重みは、$A$ の進入集合のうち $B$ へと導く部分の体積を、$A$ の進入集合の総体積で割ったものに対応する。これにより、QDAAは離散時間マルコフ連鎖へと変換される。
4. 離散化と近似： 計算を可能にするため、連続的な体積は、ファセットを均一なグリッドである $\kappa$-タイルに離散化することで近似される。数値シミュレーションを用いて、進入領域と焦点部分集合を特定する。パラメータ $\kappa$ は、離散化の粒度を制御する。
5. 収束性： 本手法は、離散化パラメータ $\kappa$ が増加するにつれて、近似体積測度が連続体積測度に収束するように設計されており、それによって元の連続的な振る舞いと近似との間の不一致を減少させる。

主な貢献
本論文は、主に4つの貢献を提示している。

1. 新しい計算手法： マルチアフィン動的システムの有限離散近似のためのQDAAの導入。この手法は、標準的な長方形抽象化に局所的なメモリ（進入集合）と定量的重みを付加したものである。
2. 収束性の証明： 離散化パラメータ $\kappa$ が無限大に近づくにつれて、QDAAが元の連続システムの振る舞いに収束することの理論的な実証（定理3.3）。
3. 到達可能性アルゴリズム： QDAAの到達可能状態空間を計算するための特定のアルゴリズム（アルゴリズム1および2）の開発。これらのアルゴリズムは、後退シミュレーション（進入集合を精緻化するため）を含む幅優先探索と数値シミュレーションを利用して、後続状態と遷移重みを決定する。
4. 実証的評価： 振動型のロトカ・ヴォルテラ変種、酵素反応速度論モデル、および大腸菌（E. coli）におけるアンモニウム同化に関する実世界のケーススタディを含む、いくつかの生物学的モデルへの適用と評価。

結果
著者らは、2次元、4次元、および7次元のモデルに対して手法を評価した。

• 振動モデルおよび酵素モデル： 結果は、$\kappa$ を増やすことで到達可能性解析の精度が向上することを示した。振動モデルにおいて、QDAAは、到達可能空間を位相空間全体へと過剰近似してしまう標準的な長方形抽象化と比較して、より正確な到達可能状態の表現を提供した。
• 大腸菌ケーススタディ： アンモニウム輸送モデルにおいて、細胞内アンモニウム濃度（$NH_4in$）に関するQDAAの結果は、標準的な長方形抽象化よりも数値シミュレーションデータに有意に近かった。QDAAの結果はシミュレーションの1桁以内の範囲であったのに対し、長方形抽象化は境界を大幅に過剰近似していた。
• 偽の振る舞い： 評価により、QDAAが、保守的な長方形抽象化に固有の偽の振る舞い（到達可能性における偽陽性）を効果的に減少させることが確認された。

意義と主張
本論文は、提案された手法が、複雑なシステムに形式的手法を適用するための実用的な転換を提供すると主張している。数値シミュレーションと長方形抽象化を組み合わせることで、QDAAは純粋な過剰近似でも過小近似でもない、中間的なアプローチを取る。その代わりに、精度のレベルを調整可能なパラメータ化された近似を提供する。

著者らは、本手法が複雑な生化学的動的システムにおける到達可能性を近似するのに十分であると断言している。これは、以下の2つの潜在的な役割を果たす。

1. 動態のグローバルな視点を得るための、パラメータ化されたシミュレーション技術としての役割。
2. 長方形抽象化と併用して、モデル検査における偽の反例を定量化し排除するためのツールとしての役割。

本研究は、会議論文のフルバージョンとして提示されており、低・中次元の生物学的モデルにおける到達可能性計算において満足のいく結果を示す理論的基礎とプロトタイプ実装（C++）を提供している。著者らは、今後の課題として、既存のモデル検査ソフトウェアへの統合、および高次元システムを扱うための並列アルゴリズムの開発を挙げている。