Bisimulation Contractions

We propose a novel algorithm for epistemic planning based on dynamic epistemic logic (DEL). The novelty is that we limit the depth of reasoning of the planning agent to an upper bound $b$, meaning that the planning agent can only reason about higher-order knowledge to at most (modal) depth $b$. We then compute a plan requiring the lowest reasoning depth by iteratively incrementing the value of $b$. The algorithm relies at its core on a new type of “canonical” $b$-bisimulation contraction that guarantees unique minimal models by construction. This yields smaller states wrt. standard bisimulation contractions, and enables to efficiently check for visited states. We show soundness and completeness of our planning algorithm, under suitable bounds on reasoning depth, and that, for a bound $b$, it runs in $(b{+}1)$-EXPTIME. We implement the algorithm in a novel epistemic planner, DAEDALUS, and compare it to the EFP 2.0 planner on several benchmarks from the literature, showing effective performance improvements.

Bisimulations are standard in modal logic and, more generally, in the theory of state-transition systems. The quotient structure of a Kripke model with respect to the bisimulation relation is called a bisimulation contraction. The bisimulation contraction is a minimal model bisimilar to the original model, and hence, for (image-)finite models, a minimal model modally equivalent to the original. Similar definitions exist for bounded bisimulations ($k$-bisimulations) and bounded bisimulation contractions. Two finite models are $k$-bisimilar if and only if they are modally equivalent up to modal depth $k$. However, the quotient structure with respect to the $k$-bisimulation relation does not guarantee a minimal model preserving modal equivalence to depth $k$. In this paper, we remedy this asymmetry to standard bisimulations and provide a novel definition of bounded contractions called rooted $k$-contractions. We prove that rooted $k$-contractions preserve $k$-bisimilarity and are minimal with this property. Finally, we show that rooted $k$-contractions can be exponentially more succinct than standard $k$-contractions.