{"ID":2824268,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2512.23324","arxiv_id":"2512.23324","title":"On Conformant Planning and Model-Checking of $\\exists^*\\forall^*$ Hyperproperties","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.","short_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. Hyp...","url_abs":"https://arxiv.org/abs/2512.23324","url_pdf":"https://arxiv.org/pdf/2512.23324v1","authors":"[\"Raven Beutner\",\"Bernd Finkbeiner\"]","published":"2025-12-29T09:20:29Z","proceeding":"cs.AI","tasks":"[\"cs.AI\",\"cs.LO\"]","methods":"[]","has_code":false}