SMCDEL.Other.Planning

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.

Generic Planning functions and type classes

class IsPlan a where

Minimal complete definition

reaches

Methods

reaches :: a -> Form -> Form

A formula saying that the given plan reaches the given goal.

reachesOn :: Semantics o => a -> Form -> o -> Bool

Instances

IsPlan OfflinePlan

Defined in SMCDEL.Other.Planning

Methods

reaches :: OfflinePlan -> Form -> Form

reachesOn :: Semantics o => OfflinePlan -> Form -> o -> Bool

Typeable a => IsPlan (ICPlan a)

Defined in SMCDEL.Other.Planning

Methods

reaches :: ICPlan a -> Form -> Form

reachesOn :: Semantics o => ICPlan a -> Form -> o -> Bool

IsPlan (Plan Form)

Defined in SMCDEL.Other.Planning

Methods

reaches :: Plan Form -> Form -> Form

reachesOn :: Semantics o => Plan Form -> Form -> o -> Bool

IsPlan (Plan MultipointedEvent)

Defined in SMCDEL.Other.Planning

Methods

reaches :: Plan MultipointedEvent -> Form -> Form

reachesOn :: Semantics o => Plan MultipointedEvent -> Form -> o -> Bool

Sequential Plans with Public Announcements

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} \]

type OfflinePlan = [Form]

A list of announcements to be made.

offlineSearch

Arguments

:: (Eq a, Semantics a, Update a Form)

=> Int

maximum number of actions

-> a

starting model or structure

-> [Form]

available actions (as public announcements)

-> [Form]

intermediate goals / safety formulas

-> Form

goal

-> [OfflinePlan]

Depth-first search for sequential public announcement plans.

Policy Plans with General Actions

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.

data Plan a

A plan with choice, i.e. a policy.

Constructors

Stop

Stop.

Do String a (Plan a)

Do a given action.

Check Form (Plan a)

Check that a formula holds. (If not, fail.)

IfThenElse Form (Plan a) (Plan a)

If ... then ... else ... .

Instances

Show a => Show (Plan a)

Defined in SMCDEL.Other.Planning

Methods

showsPrec :: Int -> Plan a -> ShowS

show :: Plan a -> String

showList :: [Plan a] -> ShowS

Eq a => Eq (Plan a)

Defined in SMCDEL.Other.Planning

Methods

(==) :: Plan a -> Plan a -> Bool

(/=) :: Plan a -> Plan a -> Bool

Ord a => Ord (Plan a)

Defined in SMCDEL.Other.Planning

Methods

compare :: Plan a -> Plan a -> Ordering

(<) :: Plan a -> Plan a -> Bool

(<=) :: Plan a -> Plan a -> Bool

(>) :: Plan a -> Plan a -> Bool

(>=) :: Plan a -> Plan a -> Bool

max :: Plan a -> Plan a -> Plan a

min :: Plan a -> Plan a -> Plan a

IsPlan (Plan Form)

Defined in SMCDEL.Other.Planning

Methods

reaches :: Plan Form -> Form -> Form

reachesOn :: Semantics o => Plan Form -> Form -> o -> Bool

IsPlan (Plan MultipointedEvent)

Defined in SMCDEL.Other.Planning

Methods

reaches :: Plan MultipointedEvent -> Form -> Form

reachesOn :: Semantics o => Plan MultipointedEvent -> Form -> o -> Bool

execute :: Update state a => Plan a -> state -> Maybe state

Try to execute a policy plan on a given state.

dix :: DynamicOp -> Form -> Form

The \(((\alpha))\phi := \langle \alpha \rangle \land [\alpha] \phi\) abbreviation from [EBMN 2017]. We call it dix because it is a combination of diamond and box.

Planning Tasks

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.

data Task state action

Constructors

Task state [(String, action)] Form

Instances

(Show state, Show action) => Show (Task state action)

Defined in SMCDEL.Other.Planning

Methods

showsPrec :: Int -> Task state action -> ShowS

show :: Task state action -> String

showList :: [Task state action] -> ShowS

(Eq state, Eq action) => Eq (Task state action)

Defined in SMCDEL.Other.Planning

Methods

(==) :: Task state action -> Task state action -> Bool

(/=) :: Task state action -> Task state action -> Bool

(Ord state, Ord action) => Ord (Task state action)

Defined in SMCDEL.Other.Planning

Methods

compare :: Task state action -> Task state action -> Ordering

(<) :: Task state action -> Task state action -> Bool

(<=) :: Task state action -> Task state action -> Bool

(>) :: Task state action -> Task state action -> Bool

(>=) :: Task state action -> Task state action -> Bool

max :: Task state action -> Task state action -> Task state action

min :: Task state action -> Task state action -> Task state action

findPlan :: (Eq state, Update state action) => Int -> Task state action -> [Plan action]

Perspective Shifts

class Eq o => HasPerspective o where

Minimal complete definition

asSeenBy

Methods

asSeenBy :: o -> Agent -> o

isLocalFor :: o -> Agent -> Bool

Instances

HasPerspective MultipointedModel

Here we also implement perspective shifts in K. The authors of [EBMN 2017] only consider S5. Given a multipointed Kripke model $(M,s)$, let the local state of $i$ be: \[ s^i := \{ w \in W \mid \exists v \in s : v R_i w \} \] Intuitively, these are all worlds the agent considers possible if the current state is $s$.

Defined in SMCDEL.Other.Planning

Methods

asSeenBy :: MultipointedModel -> Agent -> MultipointedModel

isLocalFor :: MultipointedModel -> Agent -> Bool

HasPerspective MultipointedModelS5

See ...

Defined in SMCDEL.Other.Planning

Methods

asSeenBy :: MultipointedModelS5 -> Agent -> MultipointedModelS5

isLocalFor :: MultipointedModelS5 -> Agent -> Bool

HasPerspective MultipointedBelScene

See ...

Defined in SMCDEL.Other.Planning

Methods

asSeenBy :: MultipointedBelScene -> Agent -> MultipointedBelScene

isLocalFor :: MultipointedBelScene -> Agent -> Bool

HasPerspective MultipointedKnowScene

We can also make perspective shifts symbolically. In the S5 setting we can exploit symmetry as follows. Suppose we have a multipointed scene $(F,sigma)$ where $sigma in Lng_B(V)$ encodes the set of actual states. As usual, we assume that agent $i$ has the observational variables $O_i$. Then the perspective of $i$ is given by: \[ \sigma^i := \exists (V \setminus O_i) \sigma \] On purpose we do not use $theta$ in order to avoid redundancy in the resulting multipointed scene.

Defined in SMCDEL.Other.Planning

Methods

asSeenBy :: MultipointedKnowScene -> Agent -> MultipointedKnowScene

isLocalFor :: MultipointedKnowScene -> Agent -> Bool

(HasPerspective state, Eq action) => HasPerspective (CoopTask state action)

Defined in SMCDEL.Other.Planning

Methods

asSeenBy :: CoopTask state action -> Agent -> CoopTask state action

isLocalFor :: CoopTask state action -> Agent -> Bool

Perspective Shits in 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.

Perspective Shits in K

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.

flipRelBdd :: [Prp] -> RelBDD -> RelBDD

Simultaneously prime and unprime all its variables. (TODO: subst) Formally, the resulting BDD is \( \Omega_i^\smile := \subst{V \cup V'}{V' \cup V} \Omega_i \).

Implicit Cooperation

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

data CoopTask state action

Constructors

CoopTask state [Owned action] Form

Instances

(Show state, Show action) => Show (CoopTask state action)

Defined in SMCDEL.Other.Planning

Methods

showsPrec :: Int -> CoopTask state action -> ShowS

show :: CoopTask state action -> String

showList :: [CoopTask state action] -> ShowS

(Eq state, Eq action) => Eq (CoopTask state action)

Defined in SMCDEL.Other.Planning

Methods

(==) :: CoopTask state action -> CoopTask state action -> Bool

(/=) :: CoopTask state action -> CoopTask state action -> Bool

(Ord state, Ord action) => Ord (CoopTask state action)

Defined in SMCDEL.Other.Planning

Methods

compare :: CoopTask state action -> CoopTask state action -> Ordering

(<) :: CoopTask state action -> CoopTask state action -> Bool

(<=) :: CoopTask state action -> CoopTask state action -> Bool

(>) :: CoopTask state action -> CoopTask state action -> Bool

(>=) :: CoopTask state action -> CoopTask state action -> Bool

max :: CoopTask state action -> CoopTask state action -> CoopTask state action

min :: CoopTask state action -> CoopTask state action -> CoopTask state action

(HasPerspective state, Eq action) => HasPerspective (CoopTask state action)

Defined in SMCDEL.Other.Planning

Methods

asSeenBy :: CoopTask state action -> Agent -> CoopTask state action

isLocalFor :: CoopTask state action -> Agent -> Bool

Implicitly coordinated sequential plans

As done in section 3.2 of [EBMN 2017].

type Labelled a = (String, a)

Helper type to label actions with strings.

type Owned action = (Agent, Labelled action)

An owned action is a pair of an agent and a labelled action.

type ICPlan action = [Owned action]

An implicitly coordinated plan is a sequence of owned actions. Note: there is no check that the action is actually local for the agent!

ppICPlan :: ICPlan action -> String

Pretty print an IC plan.

icSolves :: (Typeable action, Semantics state) => ICPlan action -> CoopTask state action -> Bool

Check that the given IC plan solves the given Coop task.

findSequentialIcPlan :: (Typeable action, Eq state, Update state action) => Int -> CoopTask state action -> [ICPlan action]

Depth-first search for sequential IC plans.

findSequentialIcPlanBFS :: (Typeable action, Eq state, Update state action) => Int -> CoopTask state action -> Maybe (ICPlan action)

Breadth-first search for shortest IC plans.