On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties

• URL: http://arxiv.org/abs/2512.23324v1
• Date: Mon, 29 Dec 2025 09:20:29 GMT
• Title: On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
• Authors: Raven Beutner, Bernd Finkbeiner,
• Abstract summary: We show that model-checking of hyperproperties is closely related to the problem of computing a conformant plan.<n> Firstly, we show that we can efficiently reduce a hyperproperty model-checking instance to a conformant planning instance.<n> Secondly, we establish the converse direction: Every conformant planning problem is, itself, a hyperproperty model-checking task.
• Score: 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.

Related papers

• MagicAgent: Towards Generalized Agent Planning [73.21129030631421]
  We present textbfMagicAgent, a series of foundation models specifically designed for generalized agent planning.<n>We introduce a lightweight and scalable synthetic data framework that generates high-quality trajectories across diverse planning tasks.<n>We show that MagicAgent-32B and MagicAgent-30B-A3B achieve superior performance across diverse open-source benchmarks.
  arXiv  Detail & Related papers  (2026-02-22T01:39:16Z)
• Symbolic Pattern Temporal Numeric Planning with Intermediate Conditions and Effects [6.600299648478795]
  A Symbolic Pattern Planning (SPP) approach was proposed for numeric planning where a pattern suggests a causal order between actions.<n>In this paper, we extend the SPP approach to the temporal planning with Intermediate Conditions and Effects (ICEs) fragment.
  arXiv  Detail & Related papers  (2026-02-10T14:03:40Z)
• Counterfactual Scenarios for Automated Planning [12.720308658692892]
  Counterfactual Explanations (CEs) are a powerful technique used to explain Machine Learning models.<n>We propose a novel explanation paradigm that is based on counterfactual scenarios.<n>We show that producing counterfactual scenarios is often only as expensive as computing a plan for $P$.
  arXiv  Detail & Related papers  (2025-08-29T11:16:17Z)
• GTA1: GUI Test-time Scaling Agent [97.58177633084915]
  Graphical user interface (GUI) agents autonomously complete tasks across platforms (eg, Linux) by sequentially decomposing user instructions into action proposals.<n>This paper investigates the aforementioned challenges with our textbfGUI textbfTest-time Scaling textbfAgent, namely GTA1.
  arXiv  Detail & Related papers  (2025-07-08T08:52:18Z)
• Improving Large Language Model Planning with Action Sequence Similarity [50.52049888490524]
  In this work, we explore how to improve the model planning capability through in-context learning (ICL)<n>We propose GRASE-DC: a two-stage pipeline that first re-samples high AS exemplars and then curates the selected exemplars.<n>Our experimental result confirms that GRASE-DC achieves significant performance improvement on various planning tasks.
  arXiv  Detail & Related papers  (2025-05-02T05:16:17Z)
• Plan-over-Graph: Towards Parallelable LLM Agent Schedule [53.834646147919436]
  Large Language Models (LLMs) have demonstrated exceptional abilities in reasoning for task planning.<n>This paper introduces a novel paradigm, plan-over-graph, in which the model first decomposes a real-life textual task into executable subtasks and constructs an abstract task graph.<n>The model then understands this task graph as input and generates a plan for parallel execution.
  arXiv  Detail & Related papers  (2025-02-20T13:47:51Z)
• Non-Deterministic Planning for Hyperproperty Verification [4.726777092009553]
  We show that planning offers a powerful intermediate language for the automated verification of hyperproperties. We present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem.
  arXiv  Detail & Related papers  (2024-05-22T09:57:49Z)
• Monitoring Second-Order Hyperproperties [4.099848175176399]
  We study the monitoring of complex hyperproperties at runtime. We present the first monitoring algorithm for the much more expressive class of second-order hyperproperties. We show that the monitoring of the second-order hyperproperties of Hyper$2$LTL$_f$ can be reduced to monitoring first-order hyperproperties.
  arXiv  Detail & Related papers  (2024-04-15T10:33:39Z)
• Planning as In-Painting: A Diffusion-Based Embodied Task Planning Framework for Environments under Uncertainty [56.30846158280031]
  Task planning for embodied AI has been one of the most challenging problems. We propose a task-agnostic method named 'planning as in-painting' The proposed framework achieves promising performances in various embodied AI tasks.
  arXiv  Detail & Related papers  (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" is an interactive planning approach based on Large Language Models (LLMs) DEPS facilitates better error correction on initial LLM-generated $textitplan$ by integrating $textitdescription$ of the plan execution process. Experiments mark the milestone of the first zero-shot multi-task agent that can robustly accomplish 70+ Minecraft tasks.
  arXiv  Detail & Related papers  (2023-02-03T06:06:27Z)
• Sequence-Based Plan Feasibility Prediction for Efficient Task and Motion Planning [36.300564378022315]
  We present a learning-enabled Task and Motion Planning (TAMP) algorithm for solving mobile manipulation problems in environments with many articulated and movable obstacles. The core of our algorithm is PIGINet, a novel Transformer-based learning method that takes in a task plan, the goal, and the initial state, and predicts the probability of finding motion trajectories associated with the task plan.
  arXiv  Detail & Related papers  (2022-11-03T04:12:04Z)
• STRIPS Action Discovery [67.73368413278631]
  Recent approaches have shown the success of classical planning at synthesizing action models even when all intermediate states are missing. We propose a new algorithm to unsupervisedly synthesize STRIPS action models with a classical planner when action signatures are unknown.
  arXiv  Detail & Related papers  (2020-01-30T17:08:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.