Here we provide some wrapper functions for epistemic planning via model checking. Our main inspiration for this are the following references.

• [LPW 2011] Benedikt Löwe, Eric Pacuit, and Andreas Witzel (2011): DEL Planning and Some Tractable Cases. LORI 2011. https://doi.org/10.1007/978-3-642-24130-7_13
• [EBMN 2017] Thorsten Engesser, Thomas Bolander, Robert Mattmüller, and Bernhard Nebel (2017): Cooperative Epistemic Multi-Agent Planning for Implicit Coordination. Ninth Workshop on Methods for Modalities. https://doi.org/10.4204/EPTCS.243.6

NOTE: This module is still experimental and under development.

We first consider sequential plans which are list of formulas to be publicly and truthfully announced, one after each other. These are also called offline plans. We write \(\sigma\) for any sqeuential plan and \(\epsilon\) for the empty plan which does nothing. The following then defines a formula which says that the given plan reaches a given goal \(\gamma\):

\[ \begin{array}{ll} \mathsf{reaches}(\epsilon)(\gamma) & := & \gamma \\ \mathsf{reaches}(\phi;\sigma)(\gamma) & := & \langle \phi \rangle (\mathsf{reaches}(\sigma)(\gamma)) \end{array} \]

A policy, also called online plan can include tests and choices, to decide which action to do depending on the results of previous announcements. To represent such plans we use a tree where non-terminal nodes are actions to be done or formulas to be checked. Each action node has one outgoing edge and each checking node has two outgoing edges, leading to the follow-up plans. Terminal-nodes are stop signals.

In contrast to the previous section we now also allow more general actions, namely any type in the Update class, for example action models and transformers.

A planning task (also called a planning problem) is given by a start, a list of actions and a goal. Note that texttt{state} and texttt{action} here are type variables, because we use polymorphic functions for explicit and symbolic planning in K and S5.

Given a multipointed S5 model \((\M,s)\), the local state of an agent \(i\) is given by \[ s^i := \{ w \in W \mid \exists v \in s : v \sim_i w \} \] This is the definition given in [EBMN 2017] and implemented by asSeenBy.

Note that in S5 we always have \(s \subseteq s^i\), but this is not the case in general for K. Also note that \((\cdot)^i\) is no longer idempotent if \(R_i\) is not transitive.

For the K setting we first need a way to flip the direction of the encoded relation \(\Omega_i\). This is done by fliRelBdd.

Suppose we have a set of actual states encoded by \(\sigma \in \mathcal{L}_B(V)\). Then the perspective of agent \(i\) is given by:

\[ \sigma^i := \exists V' (\Omega_i^\smile \land \sigma') \]

The following chain of equivalences shows that this definition does indeed what we want. A state \(s\) satisifes the encoding of the local state \(\sigma^i\) iff it can be reached from a state \(t\) which satisfies the encoding of the global state \(\sigma\).

\[ \begin{array}{rl} & s \vDash \sigma^i \\ \iff & s \vDash \exists V' (\Omega_i^\smile \land \sigma') \\ \iff & \exists t \subseteq V : s \cup t' \vDash (\Omega_i^\smile \land \sigma') \\ \iff & \exists t \subseteq V : t \cup s' \vDash (\Omega_i \land \sigma ) \\ \iff & \exists t \subseteq V : t \vDash \sigma \text{ and } t \cup s' \vDash \Omega_i \end{array} \]

Again we do not include \(\theta\) here to avoid redundancy in the multipointed structure.

We now introduce owner functions as discussed in [EBMN 2017] and based on [LPW 2011]

As done in section 3.2 of [EBMN 2017].