Single agent · knowledge
One robot, one accessibility relation, and a crate it may lift only where it knows the crate is. It is the degenerate case of the multi-agent domains: there is no observability to declare, and the epistemic content of the domain resides in the modal preconditions of its actions.
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
An epistemic state for a single agent is a pointed Kripke model \(M = (W, R, V, W^{*})\): the worlds the agent considers possible, one indistinguishability relation, a valuation, and the designated set of candidates for the world that is the case. Knowledge is \(\mathrm{S5}\), so \(R\) is an equivalence and \(W\) partitions into cells the agent cannot tell apart.
The modality quantifies over the cell the agent is in, which gives the two facts the domain below is built on. Sensing splits a cell, and its designated events are the readings it can return. Ontic change moves the point within a cell and leaves the partition alone.
\(M, w \models K\varphi \iff \text{for all } v,\; wRv \implies M, v \models \varphi\)
With one agent there is no observability to declare. Every event is observed by the only agent there is, so each action type in the intermediate library collapses to its public form, and the frame is \(\mathrm{S5}\) at every reachable state. The epistemic content of the domain therefore lies in the modal preconditions.
The domain
Two bays, one crate, one robot, one dock. The crate is in one of the two bays and the robot does not know which. The action that lifts it carries a modal precondition:
(:event e-pickup
:parameters (?i - agent ?z - zone)
:precondition
(and (at-ag ?i ?z) (bay ?z) (crate-at ?z) ([?i] (crate-at ?z))
(not (carrying ?i)))
:effects
(:and (carrying ?i) (not (crate-at ?z))))The conjunct \(([?i]\ (\textrm{crate-at}\ ?z))\) carries the epistemic content of the domain. Without it the encoding reduces to the classical one: an agent located at the correct bay may lift a crate it has no reason to believe is there, and a plan containing no inspection validates. With it, the lift is applicable only once the agent knows the location.
The inspection is a sensing action with two designated events, one per reading. Its observability line is the degenerate one:
(:action inspect
:parameters (?i - agent ?z - zone)
:action-type (public-sensing
(e-inspect-found ?i ?z)
(e-inspect-empty ?i ?z))
:observability-conditions (default Fully))Grounding and search
plank parses, type-checks and grounds the specification; Aletheia searches it. The numbers below are that pipeline run on the instance in instances/problem_1.epddl.
| quantity | value |
|---|---|
| frame reported by the parser | \(\mathrm{S5}\) (knowledge) |
| agents | 1 |
| grounded atoms | 23 |
| worlds in the initial state | 2 |
| designated worlds | 1 |
| grounded actions | 18 |
| strategy selected | AO*, on the sensing-small-designated rule |
| heuristic selected | epistemic distance |
| solution depth | 5 |
| nodes expanded | 52 |
| nodes generated | 48 |
| validator | OK, 1 leaf, 5 branches checked |
The returned plan is a sequence: go to the bay, inspect it, pickup, go back, unload. It contains an inspection whose reading is never branched on, which is what a single designated world buys: the model carries the agent's uncertainty, and the plan only has to be correct where the world actually is. The inspection is still required, because the lift is guarded by \([?i]\), and the agent does not know the location until it has looked.
Making the model multi-pointed, so that the actual world is itself one of several, is what turns the sequence into a policy with a branch. That instance is the immediate extension of this domain and is not yet solved: the search reports its space exhausted at a depth below the length of the evident plan. It is recorded as an open item.
The update
The inspection is one application of the product update, and it is small enough to be drawn in full. Its event model has one event per reading, both designated, and the only agent observes which one occurred. This choice of observability is the only respect in which the present case differs from the other three.
Nothing is added and nothing is removed: two worlds before, two worlds after, because each reading is applicable at exactly one of them and the two survive as \((w_0, \textsf{e-inspect-found})\) and \((w_1, \textsf{e-inspect-empty})\). What changes is the relation. \(Q_{\texttt{r}}\) is the identity on the two events, so a pair of product worlds is related only when their events agree, and the edge between the two worlds does not survive. Both self-loops do.
This is the characteristic behaviour of sensing in \(\mathrm{S5}\): the partition is refined and never coarsened, no world is excluded, and reflexivity is untouched, so nothing the agent comes to believe can be false. The same figure on the three pages beside this one is the same construction with a different \(Q_i\), and it is the choice of \(Q_i\) alone that decides whether the frame stays here or leaves for \(\mathrm{KD45}\).
The plan
A plan lists its actions but not the reason for each. That reason is found in the intermediate states, and the solution is therefore replayed here through the product 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),\)
\(V'(w,e) = \{p : \mathcal{M}, w \models \mathrm{post}_e(p)\} \cup \{p \in V(w) : \mathrm{post}_e(p)\ \text{undefined}\},\)
and the extension \([\![\varphi]\!]^{\mathcal{M}} = \{w \in W : \mathcal{M}, w \models \varphi\}\) of each formula is computed in the model the node it labels is given. An event is applicable at a state exactly when \(W^{*} \subseteq [\![\mathrm{pre}(e)]\!]\), so applicability is a containment and is read off the same picture as the goal.
Two quantities move, and they move independently. The inspection removes no world: \(|W| = 2\) before it and \(|W| = 2\) after. What it removes is two of the four edges of \(R_{\texttt{r}}\), which refines the partition \(\{\{w_0, w_1\}\}\) into \(\{\{w_0\},\{w_1\}\}\). This refinement constitutes the epistemic content of the action.
| subformula | 0initial state|W| = 2 | 1go|W| = 2 | 2inspect|W| = 2 | 3pickup|W| = 1 | 4go|W| = 1 | 5unload|W| = 1 |
|---|---|---|---|---|---|---|
| \(\texttt{crate-at}\_\texttt{bay2}\) | ||||||
| \(K_{\texttt{r}}\,\texttt{crate-at}\_\texttt{bay2}\) | ||||||
| \(\gamma\) | ||||||
| \(|W|\) | 2 | 2 | 2 | 1 | 1 | 1 |
| \(|W^{*}|\) | 1 | 1 | 1 | 1 | 1 | 1 |
| \(|R_{\texttt{r}}|\) | 4 | 4 | 2 | 1 | 1 | 1 |
The pick-up carries \(([?i]\ (\textrm{crate-at}\ ?z))\) as a conjunct of its precondition, so its applicability is the containment \(W^{*} \subseteq [\![K_{\texttt{r}}\,\texttt{crate-at}\_\texttt{bay2}]\!]\). Before the inspection that reads \(\{w_0\} \subseteq \varnothing\) and fails; after it, \(\{w_0\} \subseteq \{w_0\}\) and holds. Removing the inspection from the sequence does not shorten the plan; it renders the next action inapplicable. This is the formal content of the requirement that the agent acquire the knowledge before acting on it.
The model contracts once, at the pick-up, and for a non-modal reason: the ontic conjunct \(\texttt{crate-at}\_\texttt{bay2}\) of that event's precondition holds at \(w_0\) alone, so the update keeps one world. The same event's effect then makes the atom false, which empties \([\![K_{\texttt{r}}\,\texttt{crate-at}\_\texttt{bay2}]\!]\) again. The agent has not lost the knowledge it held; the proposition it knew is no longer true. From that point the state is a singleton and every formula of the language is decided by it.
Reproduction
cd epddl-workspace/lone-inspector
plank export -d lone-inspector.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 --explain--explain reports which rule chose the strategy and the heuristic, which is how the two selections in the table above were read off.