On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
Raven Beutner, Bernd Finkbeiner
TL;DR
The paper investigates the relationship between conformant planning and model-checking of $\exists^*\forall^*$ hyperproperties in HyperLTL, showing a tight, bidirectional connection. It introduces a planning-based encoding that reduces HyperLTL verification to conformant planning for formulas with a single quantifier alternation and proves soundness and completeness, then proves that conformant planning itself can be expressed as an $\exists^*\forall^*$ hyperproperty. A prototype translates PDDL 2.1 non-deterministic planning problems into HyperLTL verification tasks and demonstrates the scalability challenges of current HyperLTL tools on these encodings, suggesting cross-domain heuristics. The work thus provides a unified view and a path to cross-pollinate planning heuristics with hyperproperty verification techniques for unbounded temporal reasoning, with all formulas expressed as $\exists^*\forall^*$ constructs and unbounded temporal semantics.
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.