On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914223599124480 |
|---|---|
| author | Beutner, Raven Finkbeiner, Bernd |
| author_facet | Beutner, Raven Finkbeiner, Bernd |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_23324 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties Beutner, Raven Finkbeiner, Bernd Artificial Intelligence Logic in Computer Science 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. |
| title | On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2512.23324 |