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

TL;DR

This paper explores the deep connection between conformant planning and the model-checking of $orall^* egthickspaceorall^*$ hyperproperties, providing reductions in both directions to unify these two areas.

Contribution

It introduces a sound and complete reduction from hyperproperty model-checking to conformant planning and shows that conformant planning problems can be viewed as hyperproperty model-checking tasks.

Findings

Efficient reduction from hyperproperty model-checking to conformant planning.

Conformant planning problems can be expressed as hyperproperty model-checking tasks.

Establishes a theoretical equivalence between the two problems.

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.