Non-Deterministic Planning for Hyperproperty Verification

TL;DR

This paper introduces a novel approach that uses non-deterministic planning, specifically QDec-POMDPs, to automate the verification of hyperproperties expressed in HyperLTL, bridging planning and formal verification.

Contribution

It presents an algorithm that encodes HyperLTL verification problems as non-deterministic planning instances, enabling automated hyperproperty verification through planning techniques.

Findings

The encoding applies to large fragments of HyperLTL.

The planning instances often reduce to classical, FOND, or POND planning problems.

Prototype implementation shows promising experimental results.

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.