Non-Deterministic Planning for Hyperproperty Verification

• URL: http://arxiv.org/abs/2405.13488v1
• Date: Wed, 22 May 2024 09:57:49 GMT
• Title: Non-Deterministic Planning for Hyperproperty Verification
• Authors: Raven Beutner, Bernd Finkbeiner,
• Abstract summary: 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.
• Score: 4.726777092009553
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem. We implement our encoding in a prototype verification tool and report on encouraging experimental results.

Related papers

• On Conformant Planning and Model-Checking of $\exists^*\orall^*$ Hyperproperties [7.09016563801433]
  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.
  arXiv  Detail & Related papers  (2025-12-29T09:20:29Z)
• DeepPlanner: Scaling Planning Capability for Deep Research Agents via Advantage Shaping [74.34061104176554]
  We propose DeepPlanner, an end-to-end RL framework that effectively enhances the planning capabilities of deep research agents.<n>Our approach shapes token-level advantage with an entropy-based term to allocate larger updates to high entropy tokens, and selectively upweights sample-level advantages for planning-intensive rollouts.
  arXiv  Detail & Related papers  (2025-10-14T20:47:05Z)
• CRISP: Complex Reasoning with Interpretable Step-based Plans [15.656686375199921]
  We introduce CRISP (Complex Reasoning with Interpretable Step-based Plans), a dataset of high-level plans for mathematical reasoning and code generation.<n>We demonstrate that fine-tuning a small model on CRISP enables it to generate higher-quality plans than much larger models using few-shot prompting.
  arXiv  Detail & Related papers  (2025-07-09T11:40:24Z)
• VerifyLLM: LLM-Based Pre-Execution Task Plan Verification for Robots [44.99833362998488]
  We propose an architecture for automatically verifying high-level task plans before their execution in simulator or real-world environments.<n>The module uses the reasoning capabilities of the Large Language Models to evaluate logical coherence and identify potential gaps in the plan.<n>We contribute to improving the reliability and efficiency of task planning and addresses the critical need for robust pre-execution verification in autonomous systems.
  arXiv  Detail & Related papers  (2025-07-07T15:31:36Z)
• PGPO: Enhancing Agent Reasoning via Pseudocode-style Planning Guided Preference Optimization [58.465778756331574]
  We propose a pseudocode-style Planning Guided Preference Optimization method called PGPO for effective agent learning.<n>With two planning-oriented rewards, PGPO further enhances LLM agents' ability to generate high-quality P-code Plans.<n>Experiments show that PGPO achieves superior performance on representative agent benchmarks and outperforms the current leading baselines.
  arXiv  Detail & Related papers  (2025-06-02T09:35:07Z)
• HypRL: Reinforcement Learning of Control Policies for Hyperproperties [0.3277163122167433]
  We propose HYPRL, a specification-guided reinforcement learning framework.<n>We apply Skolemization to manage quantifier alternations and define quantitative functions to shape rewards.<n>A suitable RL algorithm is then used to learn policies that collectively maximize the expected reward.
  arXiv  Detail & Related papers  (2025-04-07T01:58:36Z)
• Decentralized Planning Using Probabilistic Hyperproperties [0.16777183511743468]
  We use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.
  arXiv  Detail & Related papers  (2025-02-19T10:59:02Z)
• Dynamic Planning for LLM-based Graphical User Interface Automation [48.31532014795368]
  We propose a novel approach called Dynamic Planning of Thoughts (D-PoT) for LLM-based GUI agents. D-PoT involves the dynamic adjustment of planning based on the environmental feedback and execution history. Experimental results reveal that the proposed D-PoT significantly surpassed the strong GPT-4V baseline by +12.7%.
  arXiv  Detail & Related papers  (2024-10-01T07:49:24Z)
• Unlocking Reasoning Potential in Large Langauge Models by Scaling Code-form Planning [94.76546523689113]
  We introduce CodePlan, a framework that generates and follows textcode-form plans -- pseudocode that outlines high-level, structured reasoning processes. CodePlan effectively captures the rich semantics and control flows inherent to sophisticated reasoning tasks. It achieves a 25.1% relative improvement compared with directly generating responses.
  arXiv  Detail & Related papers  (2024-09-19T04:13:58Z)
• Ask-before-Plan: Proactive Language Agents for Real-World Planning [68.08024918064503]
  Proactive Agent Planning requires language agents to predict clarification needs based on user-agent conversation and agent-environment interaction. We propose a novel multi-agent framework, Clarification-Execution-Planning (textttCEP), which consists of three agents specialized in clarification, execution, and planning.
  arXiv  Detail & Related papers  (2024-06-18T14:07:28Z)
• Testing and Understanding Erroneous Planning in LLM Agents through Synthesized User Inputs [12.412286518773028]
  Large language models (LLMs) have demonstrated effectiveness in solving a wide range of tasks. LLMs are prone to making erroneous plans, especially when the tasks are complex and require long-term planning. We propose PDoctor, a novel approach to testing LLM agents and understanding their erroneous planning.
  arXiv  Detail & Related papers  (2024-04-27T08:56:45Z)
• Learning Logic Specifications for Policy Guidance in POMDPs: an Inductive Logic Programming Approach [57.788675205519986]
  We learn high-quality traces from POMDP executions generated by any solver. We exploit data- and time-efficient Indu Logic Programming (ILP) to generate interpretable belief-based policy specifications. We show that learneds expressed in Answer Set Programming (ASP) yield performance superior to neural networks and similar to optimal handcrafted task-specifics within lower computational time.
  arXiv  Detail & Related papers  (2024-02-29T15:36:01Z)
• AutoGPT+P: Affordance-based Task Planning with Large Language Models [6.848986296339031]
  AutoGPT+P is a system that combines an affordance-based scene representation with a planning system. Our approach achieves a success rate of 98%, surpassing the current 81% success rate of the current state-of-the-art LLM-based planning method SayCan.
  arXiv  Detail & Related papers  (2024-02-16T16:00:50Z)
• Embodied Task Planning with Large Language Models [86.63533340293361]
  We propose a TAsk Planing Agent (TaPA) in embodied tasks for grounded planning with physical scene constraint. During inference, we discover the objects in the scene by extending open-vocabulary object detectors to multi-view RGB images collected in different achievable locations. Experimental results show that the generated plan from our TaPA framework can achieve higher success rate than LLaVA and GPT-3.5 by a sizable margin.
  arXiv  Detail & Related papers  (2023-07-04T17:58:25Z)
• AdaPlanner: Adaptive Planning from Feedback with Language Models [56.367020818139665]
  Large language models (LLMs) have recently demonstrated the potential in acting as autonomous agents for sequential decision-making tasks. We propose a closed-loop approach, AdaPlanner, which allows the LLM agent to refine its self-generated plan adaptively in response to environmental feedback. To mitigate hallucination, we develop a code-style LLM prompt structure that facilitates plan generation across a variety of tasks, environments, and agent capabilities.
  arXiv  Detail & Related papers  (2023-05-26T05:52:27Z)
• On the Complexity of Rational Verification [5.230352342979224]
  Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system. We show that the complexity of rational verification can be greatly reduced by specifications. We provide improved results for rational verification when considering players' goals given by mean-payoff utility functions.
  arXiv  Detail & Related papers  (2022-07-06T12:56:22Z)

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.