Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Non-Deterministic Planning for Hyperproperty Verification

Raven Beutner, Bernd Finkbeiner

TL;DR

The paper addresses verifying hyperproperties expressed in HyperLTL on finite-state systems, which is challenging due to quantifier prefixes over multiple executions. It introduces a planning-based reduction, encoding HyperLTL verification as a QDec-POMDP problem that handles reachability and safety via automata (DFA/DSA) and supports factored representations to exploit planner capabilities. The key contributions include a sound reduction to planning, a prototype tool (HyPlan) for forall*exists* properties, and empirical results showing competitive performance against parity-game encodings while benefiting from scalable, factored planning. The approach enables leveraging mature non-deterministic planning techniques to verify hyperproperties and motivates further development of planning methods tailored to verification tasks. The work thus provides a practical bridge between hyperproperty verification and planning technologies, with potential impact on security analyses and information-flow policies.

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.

Non-Deterministic Planning for Hyperproperty Verification

TL;DR

The paper addresses verifying hyperproperties expressed in HyperLTL on finite-state systems, which is challenging due to quantifier prefixes over multiple executions. It introduces a planning-based reduction, encoding HyperLTL verification as a QDec-POMDP problem that handles reachability and safety via automata (DFA/DSA) and supports factored representations to exploit planner capabilities. The key contributions include a sound reduction to planning, a prototype tool (HyPlan) for forall*exists* properties, and empirical results showing competitive performance against parity-game encodings while benefiting from scalable, factored planning. The approach enables leveraging mature non-deterministic planning techniques to verify hyperproperties and motivates further development of planning methods tailored to verification tasks. The work thus provides a practical bridge between hyperproperty verification and planning technologies, with potential impact on security analyses and information-flow policies.

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.
Paper Structure (31 sections, 4 theorems, 16 equations, 1 figure, 1 table)

This paper contains 31 sections, 4 theorems, 16 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Hyperproperties and HyperLTL.
  3. HyperLTL Verification as Planning.
  4. High-Level Overview
  5. Verification as Planning.
  6. Non-Deterministic Planning.
  7. Planning Under Partial Observations.
  8. Related Work
  9. Non-Deterministic Planning.
  10. HyperLTL Verification.
  11. Preliminaries
  12. Non-Deterministic Planning
  13. Transition Systems
  14. HyperLTL
  15. Verification via Planning
  16. ...and 16 more sections

Key Result

Theorem 1

Assume $\varphi$ is a temporal reachability formula. If $\mathcal{G}_{\mathcal{T}, \varphi}^\mathit{reach}$ admits a strong plan, then $\mathcal{T} \models \varphi$.

Figures (1)

  • Figure 1: In \ref{['fig:ts']}, we depict a transition system $\mathcal{T}$ over $\mathit{AP} = \{a\}$ using directions $\mathbb{D} = \{d_A, d_B\}$. In \ref{['fig:dsa']}, we give a DSA for the LTL body $\mathop{\mathrm{\normalfont\textsf{G}}}\nolimits (a_{\pi_1} \leftrightarrow \mathop{\mathrm{\normalfont\textsf{X}}}\nolimits a_{\pi_2})$ from \ref{['ex:running']}, where we mark state $q_3$ as losing. In \ref{['fig:instance']}, we sketch the QDec-POMDP $\mathcal{G}_{\mathcal{T}, \varphi}^\mathit{safe}$ constructed for the verification instance in \ref{['ex:running']} (see \ref{['ex:planning']} for details).

Theorems & Definitions (13)

  • Definition 1
  • Example 1
  • Definition 2
  • Theorem 1
  • proof : Proof Sketch
  • Remark 1
  • Theorem 2
  • Example 2
  • Theorem 2
  • proof
  • ...and 3 more