Knowing How to Plan
This work addresses planning challenges in multi-agent systems with epistemic reasoning, though it appears incremental as it builds on existing know-how logics.
The paper tackles the problem of higher-order epistemic planning with know-how goals, such as ensuring a condition while preventing adversaries from knowing how to undermine it, by developing a PTIME algorithm for model checking over finite epistemic transition systems.
Various planning-based know-how logics have been studied in the recent literature. In this paper, we use such a logic to do know-how-based planning via model checking. In particular, we can handle the higher-order epistemic planning involving know-how formulas as the goal, e.g., find a plan to make sure p such that the adversary does not know how to make p false in the future. We give a PTIME algorithm for the model checking problem over finite epistemic transition systems and axiomatize the logic under the assumption of perfect recall.