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.

验证超性质的自动化的算法，通过构建一个非确定性多机器人规划实例，确保一个规划存在则满足验证问题。