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

Hyperproperties express the relationship between multiple executions of a
system. This is needed in many AI-related fields, such as knowledge
representation and planning, to capture system properties related to knowledge,
information flow, and privacy. In this paper, we study the monitoring of
complex hyperproperties at runtime. Previous work in this area has either
focused on the simpler problem of monitoring trace properties (which are sets
of traces, while hyperproperties are sets of sets of traces) or on monitoring
first-order hyperproperties, which are expressible in temporal logics with
first-order quantification over traces, such as HyperLTL. We present the first
monitoring algorithm for the much more expressive class of second-order
hyperproperties. Second-order hyperproperties include system properties like
common knowledge, which cannot be expressed in first-order logics like
HyperLTL.
We introduce Hyper$^2$LTL$_f$, a temporal logic over finite traces that
allows for second-order quantification over sets of traces. We study the
monitoring problem in two fundamental execution models: (1) the parallel model,
where a fixed number of traces is monitored in parallel, and (2) the sequential
model, where an unbounded number of traces is observed sequentially, one trace
after the other. For the parallel model, we show that the monitoring of the
second-order hyperproperties of Hyper$^2$LTL$_f$ can be reduced to monitoring
first-order hyperproperties. For the sequential model, we present a monitoring
algorithm that handles second-order quantification efficiently, exploiting
optimizations based on the monotonicity of subformulas, graph-based storing of
executions, and fixpoint hashing. We present experimental results from a range
of benchmarks, including examples from common knowledge and planning.

本文研究了复杂超性质的运行时监测问题，并提出了第一个适用于更具表达能力的二阶超性质的监测算法 Hyper$^2$LTL$_f$。我们探讨了并行模型和顺序模型下的监测问题，并通过优化算法提高了二阶量化的效率。实验结果验证了算法的有效性。