2025-11-15T12:40:11.869613

Formally Verified Certification of Unsolvability of Temporal Planning Problems

Wang, Abdulaziz
We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.
academic

時間計画問題の不可解性の形式的検証認証

基本情報

  • 論文ID: 2510.10189
  • タイトル: Formally Verified Certification of Unsolvability of Temporal Planning Problems
  • 著者: David Wang, Mohammad Abdulaziz (King's College London, United Kingdom)
  • 分類: cs.LO (Logic in Computer Science), cs.AI (Artificial Intelligence)
  • 発表日: 2025年10月11日 (arXiv プレプリント)
  • 論文リンク: https://arxiv.org/abs/2510.10189

要約

本論文は、時間計画問題の不可解性認証のための方法を提案している。この方法は、計画問題を時間オートマトンネットワークにエンコードし、ネットワーク上で効率的なモデル検査器を使用した後、証明書検査器を使用してモデル検査器の出力を認証するものである。本方法は認証の信頼性を優先する：定理証明器Isabelle/HOLを使用して時間オートマトンエンコーディングの実装を形式的に検証し、既存の証明書検査器（同じくIsabelle/HOLで形式的に検証）を使用してモデル検査結果を認証する。

研究背景と動機

核心問題

本研究が解決する核心問題は、時間計画問題の不可解性認証である。時間計画は、動作が持続時間を持ち、並行実行が可能なより豊かな計画形式であり、古典的計画と比較してより複雑である。

問題の重要性

  1. 信頼性要件：既存の計画システムはアルゴリズムと実装レベルで極めて複雑であり、その出力の信頼性向上が重要である
  2. 認証の困難性：可解問題と異なり（計画の実行により検証可能）、不可解性または最適性の主張は、コンパクトな証明書を得ることが難しい
  3. 指数級の複雑性：最悪の場合、このような証明書は計画タスクのサイズに対して指数級に増加する可能性がある

既存方法の限界

  1. 形式的保証の欠如：既存の時間計画不可解性検出方法は、形式的な正確性保証を欠いている
  2. 高い複雑性：最先端の時間計画アルゴリズム技術は複雑度が高く、実用的な不可解性認証スキームの設計が困難である
  3. 検証ギャップ：古典的計画で既に行われている形式的検証研究と比較して、時間計画領域ではこの点で空白がある

研究動機

本論文はエンコーディング変換方法を採用している：時間計画問題を、既に実用的な認証アルゴリズムが存在する他の計算問題（時間オートマトン）にエンコードし、定理証明器を通じてエンコーディングプロセス全体と証明書検査器を形式的に検証することで、認証の信頼性を確保する。

核心貢献

  1. 形式的検証されたエンコーディング方法：Heinzらによる時間計画から時間オートマトンへのエンコーディングを初めて形式的に検証
  2. エンジニアリング実装：WimmerおよびvonMutiusシステムと互換性のある時間オートマトン形式を生成するようにエンコーディングを適応
  3. 簡略化された意味論設計：既存の研究より単純な時間計画意味論を設計し、数学的推論を容易にし、既存意味論との等価性を証明
  4. 完全な認証フレームワーク：時間計画問題から時間オートマトンモデル検査までの完全な信頼できる認証チェーンを構築
  5. 理論的正確性保証：Isabelle/HOLでエンコーディングの正確性を証明し、強力な理論的保証を提供

方法の詳細

タスク定義

入力：時間計画問題 P = ⟨P, A, I, G⟩

  • P：命題の集合
  • A：持続動作の集合
  • I：初期状態
  • G：目標条件

出力：不可解性の形式的証明書（問題が実際に不可解な場合）

制約条件：

  • 動作は開始および終了スナップショット動作を持つ
  • 不変条件およびスケジューリング制約をサポート
  • 相互排他制約および持続時間境界を満たす

モデルアーキテクチャ

1. 時間計画の形式化

論文はまず時間計画の形式的意味論を定義する：

スナップショット動作（定義1）：

h ≡ ⟨pre(h), adds(h), dels(h)⟩

持続動作（定義2）：

a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩

ここでa⊢とa⊣はそれぞれ開始および終了スナップショット動作である。

2. 時間オートマトンエンコーディング

変数設計（定義24）：

  • 各命題pについて：二進変数vp（真値をエンコード）およびロックカウンタlp（pが真である必要のあるアクティブな動作の数を記録）
  • aa：アクティブな動作の総数
  • ps：計画状態（0=未開始、1=計画中、2=完了）

クロック設計（定義25）：

  • 各動作aに2つのクロックを割り当て：ca⊢（開始後の時間を記録）およびca⊣（終了後の時間を記録）

メインオートマトン（定義26）： 計画プロセス全体の状態遷移を制御し、初期化と目標チェックを含む。

動作オートマトン（定義27）： 各動作に対応するオートマトンで、以下の主要な遷移を含む：

  • sea：動作開始の効果適用
  • se'a：不変条件ロック
  • eea：終了前の準備
  • ee'a：動作終了の効果適用
  • iea：瞬間動作処理

3. ネットワーク構築

メインオートマトンとすべての動作オートマトンを時間オートマトンネットワークに組み合わせ（定義28）、初期構成ではすべてのオートマトンが非アクティブ状態に設定される。

技術的革新点

  1. 並行実行サポート：Heinzらがグローバルロックを使用したのとは異なり、本論文はクロック制約を使用して並行スナップショット動作実行を許可
  2. 瞬間動作処理：iea遷移の追加により、ゼロ持続時間の瞬間動作をサポート
  3. 形式的検証：このようなエンコーディングに対して初めて機械検査可能な正確性証明を提供
  4. 意味論の簡略化：形式的推論に適した時間計画意味論を設計

実験設定

形式的検証環境

  • 定理証明器：Isabelle/HOL
  • 証明書検査器：WimmerおよびvonMutiusの検証済み証明書検査器
  • 目標性質：到達可能性チェック A ⊨ EF(loc(AM) = goal)

コード規模統計

コンポーネントコード行数
抽象時間計画意味論の形式化~7,200
Muntaを使用した時間オートマトンネットワーク定義~800
定理1および関連補題の証明~8,500
リスト関連補題~1,500
合計~18,000

比較ベンチマーク

関連する形式的検証作業との規模比較：

  • 検証されたSATベースの計画器：~17,500行
  • 検証された古典的計画検証器：~3,000行
  • 検証された時間PDDL計画検証器：~6,500行

実験結果

主要な理論的結果

定理1（主要な正確性定理）： 計画πが有効であり自己重複がない場合（valid(π) ∧ no_self_overlap(π)）、アサーション A ⊨ EF(loc(AM) = goal)が成立する。

証明構造：

  1. 補題1：並行計画の実行をシミュレートする実行の構築
  2. 補題2：初期構成からエンコード状態への到達可能性
  3. 補題3：最終状態から目標構成への遷移

形式的検証の成果

  1. 完全性証明：エンコーディングの完全性を成功裏に証明し、すべての有効な計画が対応する時間オートマトンネットワークで有効な実行を見つけることができることを示した
  2. 機械検査：すべての証明がIsabelle/HOLの機械検査を通過し、最高レベルの信頼性保証を提供
  3. モジュール設計：証明構造はモジュール化されており、理解と保守が容易

エンジニアリング実装検証

エンコーディング実装は既存の検証済み証明書検査器と互換性のある形式に適応され、完全な実行可能な認証チェーンを形成している。

関連研究

古典的計画認証

  • Erikssonらは古典的計画のためのコンパクトな不可解性認証スキームを設計
  • AbdulazizおよびLammichは古典的計画の形式的検証器を提供

時間計画とモデル検査

  • DierkらはPDDLサブセットから時間オートマトンへの静的削減を実装
  • Heinzらは時間計画問題から時間オートマトンへの明示的エンコーディングを定義
  • Giganteらは理論レベルで時間計画の複雑性を研究

形式的検証方法

  • AbdulazizおよびKurzは同様の方法を使用して認証されたSATベースの計画システムを開発
  • KumarらおよびLeroyはコンパイラ検証でステップバイステップ検証エンコーディング方法を使用

結論と議論

主要な結論

  1. 実行可能性の検証：時間計画不可解性の形式的認証が実行可能であることを証明
  2. 理論的保証：定理証明器を通じて強力な正確性保証を提供
  3. エンジニアリング実装：完全な認証ツールチェーンの構築に成功

限界

  1. 入力制限：現在、既にインスタンス化された時間計画問題のみを入力として受け入れる
  2. 意味論サブセット：サポートされる意味論は検証済み計画検証器のサブセット
  3. 実行可能性：認証メカニズムはまだ完全には実行可能化されていない

将来の方向

  1. 等価性証明：本論文の意味論と既存検証器の意味論の等価性を形式的に証明することを計画
  2. 実行可能実装：実行可能な証明書検査器の開発
  3. インスタンス化検証：Helmertのデータログソルバーなどのインスタンス化アルゴリズムの形式的検証
  4. 制約緩和：自己重複なし条件を緩和する可能性の研究

深い評価

利点

  1. 理論的厳密性：時間計画不可解性認証に対して初めて機械検査可能な形式的証明を提供
  2. エンジニアリング完全性：理論フレームワークを提供するだけでなく、既存ツールとの統合も実装
  3. 方法の革新性：
    • 並行実行をサポートするエンコーディング設計
    • 瞬間動作を処理するエレガントなソリューション
    • 簡略化されたが等価な意味論設計
  4. 信頼性保証：定理証明器を通じて最高レベルの正確性保証を提供

不足

  1. 実用性の制限：
    • 事前にインスタンス化された入力が必要
    • まだ完全には実行可能ではない
    • パフォーマンス評価が不足
  2. カバレッジ範囲：時間計画のサブセットのみをサポートし、完全なPDDL機能をサポートしない
  3. スケーラビリティ：18,000行の形式的検証作業の規模は比較的大きく、保守コストが高い

影響力

  1. 学術的貢献：
    • 時間計画の形式的検証の空白を埋める
    • 不可解性認証に対する新しい理論的基礎を提供
    • 複雑なシステムの形式的検証の実行可能性を実証
  2. 実用的価値：
    • 重要なアプリケーションに対して信頼できる計画システム認証を提供
    • 他の計画形式および制約充足問題に拡張可能
    • 自動化検証ツール開発の参考となる
  3. 再現性：オープンソースのIsabelle/HOLに基づいており、理論的には完全に再現可能

適用シナリオ

  1. 重要なシステム：高い信頼性保証が必要な計画アプリケーション（航空宇宙、医療機器など）
  2. 研究ツール：時間計画研究に対する形式的検証インフラストラクチャを提供
  3. 教育用途：形式的方法と計画アルゴリズム教育のケーススタディとして
  4. ツール開発：信頼できる計画ツール開発のための理論的基礎を提供

参考文献

主要な参考文献には以下が含まれる：

  • Abdulaziz & Koller (2022)：時間計画の形式的意味論と検証器
  • Heinz et al. (2019)：時間計画から時間オートマトンへのエンコーディング
  • Wimmer & von Mutius (2020)：時間オートマトンの検証済み証明書検査器
  • Abdulaziz & Kurz (2023)：検証されたSATベースの計画システム

本論文は時間計画の形式的検証領域に重要な貢献をしており、実用性の面でまだ改善の余地があるものの、その理論的厳密性と方法の革新性は、この領域の発展に対して堅実な基礎を築いている。