将不确定动作下的规划问题与超性质验证联系起来，揭示两者本质相通。
On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
- 把超性质验证转化为确定性规划问题，保证结果正确完整。
- 所有符合规划问题都可视为超性质验证任务，反向映射成立。
- 适合研究形式验证与智能规划交叉方向的学者参考。
我们研究了规划与验证领域中两个问题的关联：一致规划（Conformant planning）与超性质（hyperproperties）的模型检验。一致规划旨在寻找一个序列计划，在动作效果存在不确定性时仍能达成目标。超性质描述系统多条执行轨迹之间的关系，例如信息流和公平性策略。本文表明，∃*∀*型超性质的模型检验与一致规划问题密切相关。首先，我们展示了如何将超性质模型检验实例高效地转化为一致规划实例，并证明该编码是正确的且完备的。其次，我们建立了反向关系：每一个一致规划问题本身就是一个超性质模型检验任务。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。