論文の概要: Formally Verified Certification of Unsolvability of Temporal Planning Problems
- arxiv url: http://arxiv.org/abs/2510.10189v1
- Date: Sat, 11 Oct 2025 11:57:25 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-14 20:23:38.927173
- Title: Formally Verified Certification of Unsolvability of Temporal Planning Problems
- Title（参考訳）: 仮設計画問題の未解決性の形式的検証
- Authors: David Wang, Mohammad Abdulaziz,
- Abstract要約: 本稿では,時間計画の不解決性検証へのアプローチを提案する。
提案手法は,計画問題をタイムドオートマトンネットワークにエンコードし,ネットワーク上で効率的なモデルチェッカーを使用し,続いて認証チェッカーを用いてモデルチェッカーの出力を認証する手法である。
- 参考スコア（独自算出の注目度）: 11.074434296452864
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract（参考訳）: 本稿では,時間計画の不解決性検証へのアプローチを提案する。
提案手法は,計画問題をタイムドオートマトンネットワークにエンコードし,ネットワーク上で効率的なモデルチェッカーを使用し,続いて認証チェッカーを用いてモデルチェッカーの出力を認証する。
我々は、定理証明器Isabelle/HOLを用いて、タイムドオートマトンへのエンコーディングの実装を正式に検証し、既存の証明チェッカー(Isabelle/HOLでも正式に検証されている)を使用して、モデル検査結果を認証する。
関連論文リスト
- Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing [0.3807314298073301]
有限状態オートマトン方言を用いて指定されたサービスアプリケーションを実現するため、tt CAREと呼ばれる分散ランタイムアプリケーションが導入された。
tt CAREの形式的モデリング、検証、テストについて詳述する。
論文 参考訳（メタデータ） (2025-01-22T15:03:25Z) - Neural Model Checking [10.376573742987917]
時間論理をモデル化するための機械学習手法を導入し,ハードウェアの形式的検証に適用する。
我々の新しいアプローチは、ニューラルネットワークを線形時間論理の形式証明証明として用いることによって、機械学習と記号推論を組み合わせる。
提案手法は,SystemVerilogで記述された標準的なハードウェア設計において,最先端の学術的,商業的なモデルチェッカーよりも優れていることを示す。
論文 参考訳（メタデータ） (2024-10-31T10:17:04Z) - Formally Certified Approximate Model Counting [25.20597060311209]
本稿では、その出力近似の品質に関する保証を正式に保証した、近似モデルカウントのための最初の認証フレームワークを提案する。
i)Isabelle/HOL証明アシスタントにおけるアルゴリズムのPAC保証の静的かつ1回限りの公式な証明、(ii)証明証明書を用いた外部CNF-XORソルバに対するApproxMCの呼び出しの動的かつ1回実行による検証。
論文 参考訳（メタデータ） (2024-06-17T11:02:04Z) - Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
機械学習の認証は、特定の条件下では、敵対的なサンプルが特定の範囲内でモデルを回避できないことを証明している。
セグメンテーションの一般的な認証方法は、平らな粒度のクラスを使い、モデルの不確実性による高い断続率をもたらす。
本稿では,複数レベルの階層内で画素を認証し,不安定なコンポーネントに対して粗いレベルに適応的に認証を緩和する,新しい,より実用的な設定を提案する。
論文 参考訳（メタデータ） (2024-02-13T11:59:43Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - Representing Timed Automata and Timing Anomalies of Cyber-Physical
Production Systems in Knowledge Graphs [51.98400002538092]
本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。
モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
論文 参考訳（メタデータ） (2023-08-25T15:25:57Z) - Towards Evading the Limits of Randomized Smoothing: A Theoretical
Analysis [74.85187027051879]
決定境界を複数の雑音分布で探索することにより,任意の精度で最適な証明を近似できることを示す。
この結果は、分類器固有の認証に関するさらなる研究を後押しし、ランダム化された平滑化が依然として調査に値することを示す。
論文 参考訳（メタデータ） (2022-06-03T17:48:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。