On the Role of Postconditions in Dynamic First-Order Epistemic Logic

TL;DR

This paper investigates how post-conditions influence the decidability of the epistemic planning problem in dynamic first-order epistemic logic, revealing that quantifier-free post-conditions ensure decidability even with infinite domains.

Contribution

It demonstrates that the decidability of the epistemic planning problem depends critically on the quantifier structure of post-conditions in DFOEL, extending previous results to infinite domains.

Findings

Decidability holds for quantifier-free post-conditions in infinite domains.

Presence of first-order quantifiers in post-conditions leads to undecidability.

Quantifier-free post-conditions enable the use of automatic structures.

Abstract

Dynamic Epistemic Logic (DEL) is a logic that models information change in a multi-agent setting through the use of action models with pre- and post-conditions. In a recent work, DEL has been extended to first-order epistemic logic (DFOEL), with a proof that the resulting Epistemic Planning Problem is decidable, as long as action models pre- and post-conditions are non-modal and the first-order domain is finite. Our contribution highlights the role post-conditions have in DFOEL. We show that the Epistemic Planning Problem with possibly infinite first-order domains is undecidable if the non-modal event post-conditions may contain first-order quantifiers, while, on the contrary, the problem becomes decidable when event post-conditions are quantifier-free. The latter result is non-trivial and makes an extensive use of automatic structures.