Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

技術要約：有限カウンタ系への還元による非同期ラウンドベース分散アルゴリズムのパラメータ化検証

1. 問題定義

本論文は、非同期ラウンドベース分散アルゴリズム（ARDAs）のパラメータ化検証を取り扱う。従来のモデル検査が、固定された数の有限状態プロセスを検証するものであるのに対し、パラメータ化検証は、任意のプロセス数 $n$（例：$n > 2t$ のようなレジリエンス条件に従うもの）に対して正当性を証明することを目指す。

ARDAsは特有の課題を提示する。プロセス数はパラメータ化されている一方で、プロセス自体は無限状態である。これは、プロセスが無制限のラウンド・インデックスのシーケンスを実行するためであり、同期がない状況下では、プロセスは現在のラウンド・インデックスをローカル状態の一部として保持しなければならない。その結果、グローバルなシステムは、パラメータ化されたプロセスの数と、無制限なラウンド・インデックスという、2つの直交する無限性の要因を持つことになる。

著者らは、単純な仕様に対するARDAsの一般的なパラメータ化検証問題が決定不能であることを確立している。さらに、既存の有限状態分散アルゴリズム（閾値オートマトンなど）や同期型ラウンドベース・アルゴリズムのフレームワークは、ARDAsの非同期かつ無限状態の性質に直接適用することはできない。

2. 手法

本研究の核心的な貢献は、ARDAsのパラメータ化検証問題を、有限カウンタ系に対するLTLモデル検査へと、健全かつ完全な還元を行うことである。これにより、一般には決定不能である問題に対して、成熟した既存のシンボリック・モデルチェッカー（nuXmvなど）を利用することが可能となる。

手法は、2つのステージに分かれた6つの健全かつ完全な変換パイプラインを通じて進行する。

ステージ1：有限カウンタ系への還元（HSC特性用）
著者らは、特定の場所へのプロセス訪問の総数をラウンドを跨いで追跡する**履歴状態カウント（HSC）**特性を定義する。そして、無限状態のラウンドベース分散遷移システム（RDTS）を、以下の4つのステップを経て有限カウンタ系へと還元する。

1. 受信メッセージ抽象化（RMA）： メッセージの受信をスタッタリング・ステップとして扱う。ガードの評価は、特定の受信履歴ではなく、ネットワークの状態に基づいて存在的に行われる。完全性は、あるガードを満たすことが同じラウンド内の将来のルールを無効にしないことを保証する単調性条件（定義1の条件3）に依存する。
2. プロセス識別抽象化（PIA）： プロセスの識別子を除去し、各場所およびラウンドにおけるプロセスの「数」のみを追跡する。これにより、アクションベースの双模倣（bisimulation）が誘導される。
3. 半同期制限（SSR）： 更新アクションのターゲットラウンドが、現在の「フロンティア」ラウンド（存在する全プロセスが占める最大ラウンド）以上となるように、更新アクションが順序付けられた実行部分集合に限定する。これは、更新の可換性を利用して、任意の実行が、同じHSCトレースを持つ半同期的な対応物を持つことを示すものである。このステップにより、追跡すべきラウンドの「関連ウィンドウ」が限定される。
4. 限定ウィンドウ抽象化（BWA）： 限定された関連ウィンドウ（サイズ $b+1$、ここで $b$ はジャンプ境界）を利用して、ウィンドウ外のラウンドのカウンタを破棄する。システムは、フロンティアラウンドに固定されたスライディング・ウィンドウのカウンタとしてエンコードされる。
   • 結果： 固定されたパラメータ値に対しては、これは1カウンタ系となる。パラメータ化された場合（すべての値に対する非交和）は、有限カウンタ系となる。

ステージ2：LTLモデル検査への還元（HSCL論理式用）
標準的なLTLモデル検査を可能にするため、著者らは標準的な合意（consensus）やリーダー選挙の特性（合意、妥当性、停止、リーダーの一意性）を表現するために設計された履歴状態カウント論理（HSCL）を導入する。HSCL検証は、以下の追加の2ステップを経てLTLへと還元される。
5. 履歴記録拡張（HRE）： BWAの状態に「履歴記録」カウンタを付加する：
* local(ℓ)：現在のフロンティアラウンドにおける場所 $\ell$ への訪問回数をカウントする。
* cumul(ℓ)：全ラウンドにわたる $\ell$ への総訪問回数をカウントする（閾値によって上限が設定される）。
* HSCL論理式は、これらのカウンタに対するGlobally ($G$) 演算子を用いたLTL論理式へと翻訳される。
6. ラウンド識別抽象化（RIA）： 明示的なフロンティアラウンド・カウンタ（$r_{max}$）を削除する。なぜなら、HSCL特性は特定のラウンド識別子には依存せず、訪問のカウントにのみ依存するためである。
* 結果： 固定されたインスタンスに対しては、これは有限状態システムとなる。パラメータ化されたインスタンスに対しては、有限カウンタ系となる。

3. 主な貢献

• 決定不能性の証明： 2カウンタマシンの停止問題への還元により、HSCL論理式に対するARDAsのパラメータ化検証が決定不能であることを証明した。
• 健全かつ完全な還元： 決定不能性にもかかわらず、著者らは特定のHSC特性に対して健全かつ完全な還元を提供している。これは、関心のある特性に関する精度を失うことなく、ARDAsの検証問題を有限カウンタ系に対するLTLモデル検査へと変換できることを意味する。
• 形式化の定義： 標準的な正当性条件（合意、妥当性、停止、リーダーの一意性）を捉えつつ、LTLへの翻訳が可能となるよう設計された、ARDAsの形式的テンプレートおよびHSCL論理を導入した。
• 実用的な適用可能性： 既存のシンボリック・モデルチェッカー（特にIC3エンジンを備えたnuXmv）が、得られた有限カウンタ系を効率的に扱えることを示した。

4. 結果

著者らは、以下の4つのケーススタディに対してこの還元を評価した：

1. クラッシュ故障を伴うBen-Orの合意アルゴリズム。
2. ビザンチン故障を伴うBen-Orの合意アルゴリズム。
3. ビザンチン故障を伴うBrachaの合意アルゴリズム。
4. Raftのリーダー選挙アルゴリズム。

実験的知見：

• nuXmvを使用し、すべてのケーススタディにおいて安全性およびライブネス特性を検証した。
• 検証時間は低く（すべての特性で15秒未満）、IC3エンジンは浅い深さ（最大深度14）に到達した。これは、還元されたシステムが扱いやすいものであることを示している。
• レジリエンス条件を意図的に弱めて故障バリアントを作成した場合、モデルチェッカーは数秒以内に反例を生成した。

5. 意義と主張

本論文は、その還元が、成熟した汎用シンボリック・モデルチェッカーを用いて非同期ラウンドベース分散アルゴリズムを検証するための形式的な一歩を提供すると主張している。

• 先行研究との比較： 特注のCEGARループや不完全な有限状態システムへの抽象化に依存する従来の接近法（層状閾値オートマトンなど）とは異なり、本手法は有限カウンタ系への健全かつ完全な還元を提供する。これにより、カスタムの検証エンジンを必要とせず、既存のツール（nuXви、IC3、有界モデル検査など）を利用できる能力が維持される。
• 範囲： 本フレームワークは、構造的な制約により以前は除外されていたリーダー選挙アルゴリズムを含む、より広範なクラスのアルゴリズムを扱うことができる。
• 謙虚な姿勢： 著者らは、有限カウンタ系に対するLTLモデル検査自体が一般には決定不能であることを認めている。しかし、その還元によって、強力で不完全なシンボリック手法を利用できることを主張しており、これは提示されたケーススタディにおいて実証された通り、実際に効果を発揮している。また、現在の実装とケーススタディは、標準的な有限の場所のシナリオに焦点を当てている（場所の数がラウンド・インデックスと共に増大する場合、還元されたシステムは無限のカウンタを持つことになるが、その点については明記されている）。

本論文は、将来の方向性として、確率的挙動（ほとんど確実に停止することの検証）を組み込むための拡張や、ラウンド・インデックスと共に場所の数が増大するアルゴリズム（DAGベースの合意など）の扱いを挙げており、これらには無限のカウンタを持つシステムの扱いが必要になることを指摘して締めくくっている。