Knowing How to Plan

TL;DR

This paper introduces a logic-based approach to know-how planning using model checking, capable of handling higher-order epistemic goals and providing a PTIME algorithm for finite systems.

Contribution

It develops a novel logic and model checking method for higher-order epistemic planning, with a PTIME algorithm and axiomatization under perfect recall.

Findings

PTIME model checking algorithm for finite systems

Axiomatization of the logic with perfect recall

Handling higher-order know-how goals

Abstract

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.