Five EPDDL domains in which telling one agent and not another leaves the
fleet holding inconsistent pictures of the same building. One of them has
been executed on an Open-RMF fleet, and the frame was measured leaving
\(\mathrm{S5}_n\) while it ran.
The four cases
Two axes: how many agents, and knowledge or belief
Adding an agent indexes the modality. Dropping the truth axiom turns
knowledge into belief. The four pages below treat the four combinations, each through a domain that reaches it. All domains places every domain of the repository in one of them.
When the fleet stops agreeing about what is the case
A multi-agent epistemic state carries one relation per agent,
\(M = (W, \{R_i\}_{i \in \mathcal{A}}, V, W^{*})\). Under
\(\mathrm{S5}_n\) every \(R_i\) is an equivalence, and an action divides
the fleet only into those who see an outcome and those who see that
something happened. No agent can hold a false belief.
An action whose event model gives some agent a \(Q_i\) linking the event
that occurred to one that did not changes this. The uninformed agent goes
on relating to a world in which nothing happened, and if that world is
not the one that obtains, its relation is no longer reflexive:
\((w,e)\,R'_i\,(v,f) \iff w R_i v \text{ and } e Q_i f\)
The frame that results is serial, transitive and Euclidean, so the agent remains consistent and introspective while holding a false belief. Two action types in the
intermediate library produce it: private
ontic change, and announcement made to some agents and not others.
One product update: the report the guest does not receive
One application of \(\mathcal{M} \otimes \mathcal{E}\), computed from the event model the domain declares and drawn from the result. A world of the product is a pair \((w, e)\) whose event is applicable at its world, and \((w,e)\,R'_i\,(v,f)\) holds exactly when \(w R_i v\) and \(f \in Q_i(e)\). The loop above a world is its reflexive edge; where that loop is missing at a designated world, the agent excludes the world that is the case.
The figure is one step of the executed
hotel-incident run: the inspector radios
its finding to the porter while the guest is on another floor. The event
model has three events and the announcement's observability is conditional
on position, so the three agents are given three different relations over
the same events. The inspector and the porter are
Fully observant and keep every self-loop;
the guest satisfies
\(\neg\texttt{at-ag}\_\texttt{guest}\_\texttt{l3}
\_\texttt{suite}\) and is therefore
Oblivious, so both real events are sent
to nil.
Selecting each agent in turn shows the effect of that difference. The model
goes from two worlds to four, and for the two informed agents the additional worlds only enlarge their relations, which gain edges and remain
\(\mathrm{S5}_n\). For the guest the designated world loses its
loop and points instead at the two \(\textsf{nil}\) copies, which
are the worlds in which no announcement was made. It is the only agent
whose relation changes in kind and not merely in size, and it is the agent the
goal's secrecy conjunct is about.
The domains
Five domains that reach \(\mathrm{KD45}_n\)
domain
action types used
what makes it doxastic
coin-in-the-box
private ontic, quasi-private sensing
an agent peeks while another is not looking
box-task
public ontic, private ontic, private announcement
a box is moved unseen
box-task-2.0
the above with public sensing
as above, with a public reading to repair it
doxastic-depot
all eight of the library's types
the goal asks for a false belief directly
hotel-incident
public ontic, semi-private sensing, private ontic,
quasi-private and public announcement
a valve shut behind a closed door
doxastic-depot states the phenomenon most directly: its first instance asks for a state in which the chief believes
a crate is still in bay 1 while it is in fact in bay 2. The goal is a
false belief, and the plan that achieves it moves the chief out of the
bay before moving the crate.
Measurement
The frame changing during a run
hotel-incident is the domain that has
been executed on a fleet, and not only solved. A leak in one of two
suites on separate floors, an inspector, a porter and a guest, and a goal
with a secrecy conjunct: the incident is to be over, the porter is to
know it, and the guest is never to learn which suite was involved.
The run was replayed against a standalone epistemic state and each
agent's accessibility relation was recorded after every action. The frame is measured from the relation, not assumed from the domain:
Figure 1. Each agent's relation counted as a graph at every step
of the hotel run. The guest's relation loses reflexivity at the private
announcement and the inspector's at the private ontic action; each
remains serial, transitive and Euclidean without it, which is
\(\mathrm{KD45}\). The porter's stays \(\mathrm{S5}\) throughout while
its edge count rises from four to seven, because the model it is
defined over grows from two worlds to five.
Two agents end the run holding beliefs the world contradicts, and both
continue to satisfy every formula their designated worlds support. The model grows: five worlds at the end against two at
the start, because each partly-observed action introduces the distinction
between what happened and what an uninformed agent still takes to be the
case.
The full execution, with the policy, the recorded run and the
step-by-step measurement, is on the
hotel incident page.
The policy
What the planner returned, and what each action costs in worlds
The solution to hotel-incident is a
policy and not a sequence, and the diagram below is read off the
planner's output and replayed through the product update. Every model in
it was checked against the models the executor measured during the run:
the reconstruction is bisimilar to the measurement at all five steps, and
reproduces every formula the executor reported.
The policy Aletheia returned, and the model at every node\(\gamma \equiv \texttt{safe} \wedge K_{\texttt{porter}}\,\texttt{safe} \wedge \neg \mathit{Kw}_{\texttt{guest}}\,\texttt{leak-at}\_\texttt{l2}\_\texttt{suite}\)
sensingonticannouncementa world at which the goal holdsa world at which it does nota designated world
2e-inspect-wet : \(\neg \mathit{Kw}_{\texttt{inspector}}\,\texttt{leak-at}\_\texttt{l2}\_\texttt{suite}\) holds at 2 of the 2 worlds of the model this action is given, and \(|W^{*}| = 2\)
2e-inspect-dry : \(\neg \mathit{Kw}_{\texttt{inspector}}\,\texttt{leak-at}\_\texttt{l2}\_\texttt{suite}\) holds at 2 of the 2 worlds of the model this action is given, and \(|W^{*}| = 2\)
3\(K_{\texttt{inspector}}\,\texttt{leak-at}\_\texttt{l2}\_\texttt{suite}\) holds at 1 of the 2 worlds of the model this action is given, and \(|W^{*}| = 1\)
4\(K_{\texttt{inspector}}\,\texttt{safe}\) holds at 1 of the 3 worlds of the model this action is given, and \(|W^{*}| = 1\)
6\(K_{\texttt{inspector}}\,\texttt{leak-at}\_\texttt{l3}\_\texttt{suite}\) holds at 1 of the 2 worlds of the model this action is given, and \(|W^{*}| = 1\)
7\(K_{\texttt{porter}}\,\texttt{leak-at}\_\texttt{l3}\_\texttt{suite}\) holds at 1 of the 4 worlds of the model this action is given, and \(|W^{*}| = 1\)
The solution as the AND-OR tree it is, drawn from the planner’s output. Beside each action is the model that action is given: one dot per world, filled where \(\gamma\) holds and ringed where the world is designated, so a row in which every ringed dot is filled is a state satisfying the goal. An action with two outgoing edges has two designated events, and the continuation below each edge is applicable only in the state that edge produces, which is what makes a solution a policy and not a sequence. The numbered notes give the modal conjuncts each action is guarded by; an action with no note has none, and is applicable on ontic grounds alone.
Three things in the diagram are consequences of the goal alone. The root
is a single event relocating two agents, because a policy is a sequence of
updates and two consecutive moves would be two updates; it commits one
robot to each floor before the location is known, which places one of them
correctly under either reading. The inspection is the only branching node,
since it is the only action with more than one designated event. And both
continuations carry the finding by private announcement, because the
public one would put the guest in
\([\![\mathit{Kw}_{\texttt{guest}}\,\texttt{leak-at}
\_\texttt{l2}\_\texttt{suite}]\!]\) and falsify the third conjunct.
The extension of each subformula of the goal, along the dry branch\(\gamma \equiv \texttt{safe} \wedge K_{\texttt{porter}}\,\texttt{safe} \wedge \neg \mathit{Kw}_{\texttt{guest}}\,\texttt{leak-at}\_\texttt{l2}\_\texttt{suite}\)
The branch the recorded run took. The model grows, and the two agents that end the run holding a false belief are the two whose relation loses an edge count it does not recover.
The measurement that distinguishes this tier from
\(\mathrm{S5}_n\) is the world count. Under \(\mathrm{S5}_n\) an
informative action can only shrink the model, because every agent's
relation is an equivalence and an event either separates two worlds for an
agent or leaves them together. Here the model grows: from two worlds to
four at the private announcement and to five at the private ontic action.
Each of those steps introduces the distinction between what happened and
what an agent that did not observe it still takes to be the case, and it
is exactly that distinction which a non-reflexive relation is needed to
represent.
Reproduction
Running them
cd epddl-workspace/doxastic-depot
plank export -d doxastic-depot.epddl -p instances/problem_1.epddl \
-l $PLANK/benchmarks/libraries/intermediate.epddl -o out
epistemic_planner --task out/problem_1.json --plan out/problem_1-plan.json
A problem reaching this tier declares
:KD45-frames in its requirements, and
the parser prints the frame it found before search begins.
