Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

技術要約：実時間システムの論理ベース解析における遅延制約（Delayed Constraints）

問題提起
実時間システムの形式的な解析は、無限性に関して2つの主要な課題に直面している。それは、エージェントやメッセージの数が無制限である可能性と、密な時間（dense time）に起因する状態空間の無限性である。Rewriting Logic (RL) を用いた従来の検証手法、特に Maude 書き換えエンジンに実装されているものは、歴史的に制限があった。Maude は、完全に指定されたコンポーネント（基底項）と SMT 制約を持つシステムに対して不変量検証をサポートしているが、未知の数のエージェントや任意のパラメータを含むシステムには苦慮する。さらに、従来の記号的手法は時間のサンプリングに依存することが多く、これは密な時間の設定においては健全性（soundness）と完全性（completeness）を欠く。無制限のエージェントを扱うために論理変数を用いる既存のアプローチは、しばしば無限の探索空間を持つ半決定手続きとなり、終了を保証するメカニズムを欠いている。

手法
著者らは、これらの制限に対処するために3つのコア技術を統合した新しい検証フレームワークを提案している。

1. Rewriting Modulo SMT: 時間制約の記号的表現のために SMT 理論を利用する。
2. 論理変数を用いたナローイング（Narrowing with Logical Variables）: 未知または任意の数のエージェントに関する推論を行うために論理変数を用いる。
3. 遅延制約とフォールディング（Delayed Constraints and Folding）: 制約論理プログラミング（CLP）に着想を得た、部分的にインスタンス化された項に対する制約ストアを導入する。

核心となる革新は**遅延フォールディング・ナローイング（Delayed Folding Narrowing）**である。標準的なナローイングとは異なり、この手法では、ルールの条件に含まれる SMT 式が「遅延」部分（項がさらにインスタンス化されるまで評価できない部分式）を含むことを許容する。これは、非妥当な SMT 式（例：最大経過時間を示す mte(t, T')）を新しい変数へと抽象化する SMT 拡張を通じて実現される。これらの制約は蓄積され、項が十分にインスタンス化された時点で初めて解決または伝播される。

本フレームワークは、以下の機能を拡張した**論理的実時間書き換え理論（Logical Real-Time Rewrite Theories）**を定義する。

• 書き換えルールの条件に、遅延部分を含む SMT 式を含めること。
• 右辺（RHS）に、左辺（LHS）に存在しない変数を含めること。
• クエリに、初期状態とターゲット状態に共通の変数を含めること。

終了性を確保するため、手法はフォールディング機構を採用している。記号的な状態 $v'$ が、等式理論（equational theory）に関して既に探索された状態のインスタンスである場合、その状態を除去することで状態グラフを構築する。著者らは、特定の条件下（具体的には、注意深く設計されたソートの階層の下）において、このフォールディング前順序が有限の探索空間を保証し、半決定手続きを不変量検証のための決定手続きへと変貌させることを証明している。

主な貢献

1. 遅延フォールディング・ナローイング: 遅延制約を持つ拡張 SMT 式を扱うナローイング関係の定義と実装。これにより、初期構成および不変量の両方において、任意の論理変数および SMT 変数を持つシステムの検証が可能となる。
2. Timed Fischer プロトコルの検証: 最も一般的な設定における、タイムド・フィッシャー相互排除プロトコルの正当性の自動検証を初めて提示した。これには、任意の数のプロセス、および任意の時間パラメータ（$\gamma$ および $\delta$）が含まれる。これは、終了手続きを保証するための特定のソート階層を設計し、未指定のプロセス数を表すために論理変数を利用することによって達成された。
3. Dining Philosophers のコントローラ合成: 本フレームワークをタイムド・ダイニング・フィロソファーズ問題に適用し、コントローラ（「lackey」）を合成した。コントローラの遷移を未指定（論理変数で表現）にすることで、到達可能性特性（例：特定のデッドライン前に特定の哲学者がダイニングルームに入る）を満たすために不足している遷移をナローイング手続きによって合成した。

結果
本手法は、メタレベルの機能を用いて Maude 書き換えエンジンの拡張として実装された。

• Fischer プロトコル: 任意の数のプロセスに対する相互排除の検証に成功した。初期状態が $\gamma > \delta$ と制約されている場合、フォールディングにより探索空間は有限（3つの状態のみ）となり、到達可能な状態がいかなる不変量違反も起こさないことが確認された。逆に、$\delta \ge \gamma$ の場合には反例が見つかった。
• Dining Philosophers: 特定の哲学者がダイニングルームに入れるようにする lackey オートマトンを正常に合成した。出力は、コントローラに必要な具体的な遷移とロケーションを提供し、到達可能性特性を満たすための不足している遷移を合成できる本フレームワークの能力を示した。
• 効率性: フォールディング機構は探索空間を大幅に縮小し、無限の状態空間のために本来は手に負えない（intractable）となるようなシステムの解析を可能にした。

意義と主張
本論文は、実時間書き換え理論の記号的検証のための、健全かつ表現力豊かな基盤を提供することを主張している。その意義は、論理プログラミングの表現力（論理変数による無制限のエージェントの扱い）と、実時間解析の精密さ（SMT と遅延制約による密な時間の扱い）の間の溝を埋めることにある。

著者らは、自身のアプローチが、固定されたプロセスの数や固定された時間境界を通常必要とする標準的な Maude や既存のパラメトリック・タイムド・オートマトン（PTA）ツールを超えたものであることを強調している。単一のフレームワーク内で任意のパラメータと無制限のエージェント数をサポートすることで、本手法は複雑な実時間モデルを分析するための統一的なアプローチを提供する。遅延制約は、無限状態の実時間システムにおける記号的解析において、終了性を達成するための極めて重要なメカニズムであることが示唆されている。