Single agent · belief
A robot commands a door it cannot observe. A single ontic action to which the only agent is oblivious suffices to separate the agent’s accessible worlds from the actual one, and so to take the frame out of \(\mathrm{S5}\) without a second agent.
The four cases
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.
The planning task
\(\mathrm{S5}\) is \(\mathrm{KT45}\). Removing T and putting D in its place gives \(\mathrm{KD45}\), the logic of belief. The modality is written \(B\), and the axioms are:
Without reflexivity the world that is the case need not lie in the agent's own accessible set, so \(B\varphi \wedge \neg\varphi\) becomes satisfiable. The agent remains consistent and fully introspective about a belief that is wrong, and for this reason the failure has to be anticipated by the planner: no formula evaluated from the agent's perspective reveals it.
With a single agent the multi-agent route to false belief, informing one agent and not another, is unavailable. The remaining route is an action whose effect the agent does not observe, and it suffices.
The domain
A robot in the office, a door in the plant, and a command that shuts the door remotely. The robot issues the command and cannot see the result. The action is ontic and the only agent is oblivious to it:
(:action command-shut
:parameters (?i - agent ?z - zone)
:action-type (private-ontic (e-command ?i ?z) (nil))
:observability-conditions (default Oblivious))The alternative event is nil, so after the update the agent still relates to a copy of the world in which nothing happened, and that copy is the one it takes itself to be in. The door is shut; the agent believes it open. The parser reports the frame accordingly.
The false belief is repaired by travelling to the plant and observing the door. It is a sensing action with one designated event per reading, and standing at the door makes the readings distinguishable:
(:action look
:parameters (?i - agent ?z - zone)
:action-type (public-sensing (e-look-shut ?i ?z) (e-look-open ?i ?z))
:observability-conditions (default Fully))The update
The command is one application of the product update, and the step is small enough to be drawn in full. The event model has two events, the one that shuts the door and nil; the only agent is oblivious, so \(Q_{\texttt{r}}\) sends the event that occurred to the one that did not. Everything the domain claims about belief follows from that single pairing.
Consider the product in the second row. The two surviving pairs are \((w_0, \textsf{e-command})\), where the door is shut, and \((w_0, \textsf{nil})\), where it is not; the first is designated, because the command is what actually happened. The relation is computed from \(w_0 R_{\texttt{r}} w_0\) together with \(\textsf{e-command}\,Q_{\texttt{r}}\,\textsf{nil}\), and those two facts give one edge, from the designated world to the other one:
\(R_{\texttt{r}}(w_0) = \{w_1\} \not\ni w_0.\)
The loop above \(w_0\) in the first row is gone in the second, and the absence of this loop is precisely what distinguishes knowledge from belief. Reflexivity is what makes \(K\varphi \to \varphi\) valid, so an agent whose relation has lost the loop at the world that obtains can satisfy \(K\varphi \wedge \neg\varphi\). The relation remains serial, transitive and Euclidean (the loop at \(w_1\) is still there, and it is the only world the agent reaches), so the frame is \(\mathrm{KD45}\) and the agent is consistent and fully introspective about a belief the world contradicts.
Grounding and search
| quantity | value |
|---|---|
| frame reported by the parser | \(\mathrm{KD45}\) (belief) |
| agents | 1 |
| grounded atoms | 9 |
| worlds in the initial state | 1 |
| grounded actions | 8 |
| goal (shut) | solved at depth 1, 3 expanded |
| goal ([r] (shut)) | unsolved; space reported exhausted at depth 3 |
The first row is the principal result of this page. The declaration alone is enough for the parser to classify the task as \(\mathrm{KD45}\): a single-agent domain with one oblivious ontic action leaves the frame non-reflexive, and belief becomes the attitude the planner reasons about.
Achieving that the door is shut requires one action. Achieving that the agent knows it is shut is not currently solved: the search reports its space exhausted at depth three, below the length of the plan that should succeed (command, drive, look). The repair path is stated in the domain and the goal is expressible, so the deficiency lies in the search and not in the model. It is recorded here as an open item.
The plan
The claim that the deficiency lies in the search and not in the model concerns two separable questions. Whether a sequence reaches the goal is decided by the product update and the satisfaction relation; whether the search finds it is decided by the search. The first is settled here by putting the three-action repair the domain states (command the door shut, drive to the plant, look) through the update
\(W' = \{(w,e) \in W \times E : \mathcal{M}, w \models \mathrm{pre}(e)\}, \qquad (w,e)\,R'_i\,(v,f) \iff w R_i v \ \text{and}\ f \in Q_i(e),\)
and evaluating the goal in each state it produces. The sequence is not a planner output and is not presented as one; it is a witness, written in the plan format so that the same tool can check it.
The command is the central step. Its event model pairs the event that shuts the door with nil, and the only agent is oblivious, so \(Q_{\texttt{r}}\) sends the event that occurred to the one that did not. The update therefore turns one world into two, and the agent's relation at the designated world points at the copy in which nothing happened:
\(R_{\texttt{r}}(w_0) = \{w_1\}, \qquad w_0 \notin R_{\texttt{r}}(w_0).\)
Reflexivity is lost at exactly that step and at exactly that world, and with it the truth axiom. What remains is serial, transitive and Euclidean, which is \(\mathrm{KD45}\), and the agent is consistent and fully introspective about a belief the world contradicts.
The domain declares one box modality and the figures write it \(K\) throughout. Whether that symbol is read as knowledge or as belief is a property of the frame and not of the notation: it is knowledge where the relation is reflexive at the designated world, and belief where it is not. The step at which the reading changes is the step at which the edge above is lost, and it can be pointed at.
| subformula | 0initial state|W| = 1 | 1command-shut|W| = 2 | 2go|W| = 2 | 3look|W| = 2 |
|---|---|---|---|---|
| \(\texttt{shut}\) | ||||
| \(K_{\texttt{r}}\,\texttt{shut}\) | ||||
| \(\neg \texttt{shut}\) | ||||
| \(K_{\texttt{r}}\,\neg \texttt{shut}\) | ||||
| \(\gamma\) | ||||
| \(|W|\) | 1 | 2 | 2 | 2 |
| \(|W^{*}|\) | 1 | 1 | 1 | 1 |
| \(|R_{\texttt{r}}|\) | 1 | 2 | 2 | 1 |
The false belief is the third row read against the first: \(w_0\) lies in \([\![\texttt{shut}]\!]\) and in \([\![K_{\texttt{r}}\,\neg\texttt{shut}]\!]\) at the same time, so \(K_{\texttt{r}}\varphi \wedge \neg\varphi\) is satisfied at the designated world. Nothing inside the agent's own perspective distinguishes that state from the one before the command, and for that reason it has to be anticipated in planning, since it cannot be detected in execution.
The look repairs it without repairing the frame. It removes one edge, and \([\![K_{\texttt{r}}\,\texttt{shut}]\!]\) acquires \(w_0\), so the goal \(\texttt{shut} \wedge K_{\texttt{r}}\,\texttt{shut}\) holds at the designated world; \(R_{\texttt{r}}\) is still not reflexive, and the agent has come to know something without the model returning to \(\mathrm{S5}\). A solution of length three therefore exists and is exhibited, and what the search reports exhausted at depth three is its own space and not the problem's.
Reproduction
cd epddl-workspace/remote-door
plank export -d remote-door.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.jsonThe parser prints its frame verdict on the first line, which is where \(\mathrm{KD45}\) in the table above comes from.