論文の概要: On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
- arxiv url: http://arxiv.org/abs/2512.23324v1
- Date: Mon, 29 Dec 2025 09:20:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-30 22:37:30.450808
- Title: On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
- Title（参考訳）: $\exists^*\forall^*= hyperproperties の整合計画とモデルチェッキングについて
- Authors: Raven Beutner, Bernd Finkbeiner,
- Abstract要約: 本稿では,超越性モデル検査が適合計画の計算問題と密接に関連していることを示す。
まず, 最適モデルチェックインスタンスを適合計画インスタンスに効率よく還元できることを示す。
次に、逆方向を定め、全ての適合計画問題は、それ自体が超完全性モデルチェックタスクである。
- 参考スコア（独自算出の注目度）: 7.09016563801433
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: We study the connection of two problems within the planning and verification community: Conformant planning and model-checking of hyperproperties. Conformant planning is the task of finding a sequential plan that achieves a given objective independent of non-deterministic action effects during the plan's execution. Hyperproperties are system properties that relate multiple execution traces of a system and, e.g., capture information-flow and fairness policies. In this paper, we show that model-checking of $\exists^*\forall^*$ hyperproperties is closely related to the problem of computing a conformant plan. Firstly, we show that we can efficiently reduce a hyperproperty model-checking instance to a conformant planning instance, and prove that our encoding is sound and complete. Secondly, we establish the converse direction: Every conformant planning problem is, itself, a hyperproperty model-checking task.
- Abstract（参考訳）: 計画と検証のコミュニティにおける2つの問題の関連性について検討する。
コンフォーマント計画(Conformant Planning)は、計画の実行中に非決定論的作用から独立した目的を達成するシーケンシャルな計画を見つけるタスクである。
ハイパープロパティは、システムの複数の実行トレースに関連するシステムプロパティであり、例えば、情報フローと公正ポリシーをキャプチャする。
本稿では,$\exists^*\forall^*$ hyperpropertiesのモデルチェックが,適合計画の計算問題と密接に関連していることを示す。
まず,適応型計画インスタンスに高確率モデルチェックインスタンスを効率よく還元し,符号化が健全かつ完全であることを証明できることを示す。
次に、逆方向を定め、全ての適合計画問題は、それ自体が超完全性モデルチェックタスクである。
関連論文リスト
- GTA1: GUI Test-time Scaling Agent [97.58177633084915]
グラフィカルユーザインタフェース(GUI)は、ユーザ命令をアクションプロポーザルに順次分解することで、プラットフォーム(例えばLinux)間で自律的にタスクを完了させる。
本稿では,前述の textbfGUI textbfTest-time Scaling textbfAgent,すなわち GTA1 の課題について検討する。
論文 参考訳（メタデータ） (2025-07-08T08:52:18Z) - Improving Large Language Model Planning with Action Sequence Similarity [50.52049888490524]
本研究では,インコンテキスト学習(ICL)によるモデル計画能力の向上について検討する。
GRASE-DC は2段階のパイプラインで,まず高効率のAS例を再サンプリングし,選択した例をキュレートする。
実験の結果,GRASE-DCは様々な計画タスクにおいて大幅な性能向上を実現していることがわかった。
論文 参考訳（メタデータ） (2025-05-02T05:16:17Z) - Plan-over-Graph: Towards Parallelable LLM Agent Schedule [53.834646147919436]
大規模言語モデル(LLM)はタスク計画の推論において例外的な能力を示した。
本稿では,まず実生活のテキストタスクを実行可能なサブタスクに分解し,抽象的なタスクグラフを構築する,新しいパラダイムであるプランオーバーグラフを提案する。
モデルはこのタスクグラフを入力として理解し、並列実行計画を生成する。
論文 参考訳（メタデータ） (2025-02-20T13:47:51Z) - Non-Deterministic Planning for Hyperproperty Verification [4.726777092009553]
提案手法は,ハイパープロパティの自動検証に強力な中間言語を提供することを示す。
本稿では,HyperLTL検証問題に対して,非決定論的マルチエージェント計画インスタンスを構築するアルゴリズムを提案する。
提案手法は,HyperLTLの大きな断片に対して,従来のFOND,あるいはPOND計画問題に対応していることを示す。
論文 参考訳（メタデータ） (2024-05-22T09:57:49Z) - Monitoring Second-Order Hyperproperties [4.099848175176399]
本研究では,実行時の複雑なハイパープロパティのモニタリングについて検討する。
より表現力に富んだ2次超越性に対する最初のモニタリングアルゴリズムを提案する。
本稿では,Hyper$2$LTL$_f$の2次ハイパープロパティの監視を1次ハイパープロパティの監視に還元できることを示す。
論文 参考訳（メタデータ） (2024-04-15T10:33:39Z) - Planning as In-Painting: A Diffusion-Based Embodied Task Planning
Framework for Environments under Uncertainty [56.30846158280031]
具体的AIのためのタスクプランニングは、最も難しい問題の1つだ。
In-paintingとしての計画」というタスク非依存の手法を提案する。
提案するフレームワークは,様々な具体的AIタスクにおいて,有望なパフォーマンスを実現する。
論文 参考訳（メタデータ） (2023-12-02T10:07:17Z) - Describe, Explain, Plan and Select: Interactive Planning with Large Language Models Enables Open-World Multi-Task Agents [26.78244595330595]
「$underlineD$escribe」は、Large Language Models(LLMs)に基づく対話型計画手法である。
DEPSは、計画実行プロセスの$textitdescription$を統合することで、初期LLM生成の$textitplan$のエラー修正を容易にする。
実験は、70以上のMinecraftタスクを確実に達成できる最初のゼロショットマルチタスクエージェントのマイルストーンとなる。
論文 参考訳（メタデータ） (2023-02-03T06:06:27Z) - Sequence-Based Plan Feasibility Prediction for Efficient Task and Motion
Planning [36.300564378022315]
本稿では,移動環境における移動操作問題を解決するための学習可能なタスク・アンド・モーション・プランニング(TAMP)アルゴリズムを提案する。
本アルゴリズムのコアは,タスク計画,目標,初期状態を考慮したトランスフォーマーに基づく新しい学習手法であるPIGINetであり,タスク計画に関連する運動軌跡の発見確率を予測する。
論文 参考訳（メタデータ） (2022-11-03T04:12:04Z) - STRIPS Action Discovery [67.73368413278631]
近年のアプローチでは、すべての中間状態が欠如している場合でも、アクションモデルを合成する古典的な計画が成功している。
アクションシグネチャが不明な場合に,従来のプランナーを用いてSTRIPSアクションモデルを教師なしで合成するアルゴリズムを提案する。
論文 参考訳（メタデータ） (2020-01-30T17:08:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。