EPDDL · plank · ALETHEIA · ePlanSys · Gazebo
The warehouse run states a mission whose goal is knowledge, and every goal it states has modal depth one: some named robot must come to know whether the pallet is in a given aisle. This page keeps that domain, that floor and that fleet exactly, and varies one thing. Three EPDDL instances are identical to the last line of their initial state and differ only in the goal formula. One of the three has an operator inside another. The question is whether that alone changes what the robots do, and it does: two of the goals are discharged by the sensing action, the third is not and the planner spends an announcement on it.
Same world as the warehouse run: AWS RoboMaker's small warehouse, three TurtleBot3 burgers, the domain in epddl-workspace/robot-warehouse and the execution in ros2_ws/src/warehouse_demo. Nothing in the domain, the world or the action nodes was changed for this page; the instances and one logging node were added. Epistemic-Robotics
What this is for
The earlier page demonstrates that a goal about knowledge forces a conditional policy, and that a fleet member which never moves can still be required to know something. Both are true and neither needs a nested operator. Reading it back, four things it does not show stand out, and they have one cause.
Every goal is depth one. Each conjunct is [Kw. i] pallet-at_bay2 for some agent. No formula in the repository asks what one agent knows about another's knowledge, so nothing in the search or the execution has ever been asked to distinguish the two.
The two-agent case is discharged for free. pickup is a public ontic action whose precondition names the pallet's location, so the whole fleet observing r1 lift the pallet out of an aisle learns which aisle held it. r2's conjunct is settled by the fetch, and would be settled by it whatever the goal said. The three-agent instance does select an announcement, but what it announces is an atom, broadcast to everyone.
The semi-private sensing is invisible in the policy. The domain declares inspect as (:and (?i Fully) (default Partially)): the agent that looks learns the outcome, and the rest of the fleet learns only that an inspection occurred. That distinction is in the event model and has been since the domain was written. No goal ever depended on it, so no plan ever exhibited it.
One goal per instance. Without two goals over one world there is no controlled comparison: nothing that holds the physical trace fixed and varies only the formula.
The common cause is that no goal was ever written that needed the depth. Nothing below required a change to the domain, the planner, the epistemic state or its formula parser.
The three goals
The three instances are generated from one text and diverge at the goal. Each carries two ontic conjuncts and one modal conjunct; the ontic pair is the same in all three. In EPDDL as this project writes it, [i] φ is knowledge, [Kw. i] φ is knowing-whether, and a formula nests by appearing where φ does:
; G1 the control: the robot that looks is the one that has to know (:goal (and (at-ag r2 corridor) (at-ag r3 lane) ([Kw. r1] (pallet-at bay2)) )) ; G2 depth two: r2 has to know that r1 knows whether (:goal (and (at-ag r2 corridor) (at-ag r3 lane) ([r2] ([Kw. r1] (pallet-at bay2))) )) ; G3 depth one again, but about the robot that never looks (:goal (and (at-ag r2 corridor) (at-ag r3 lane) ([Kw. r2] (pallet-at bay2)) ))
Written as formulas, and abbreviating the two ontic literals the three share as \(\delta = \mathit{at}(r_2,\textit{corridor}) \wedge \mathit{at}(r_3,\textit{lane})\):
G3 is not a weaker G2 and G2 is not a stronger G3; they are independent. \(K_{r_2}\mathit{Kw}_{r_1}P\) says r2 has established that the question is settled for r1, and says nothing about the answer; \(\mathit{Kw}_{r_2}P\) says r2 has the answer, and says nothing about r1. Neither entails the other. In this domain the first is obtainable by watching and the second is not. What decides that is the observability declared on the sensing action.
The warehouse mission's goal conjunct (delivered) is deliberately absent. Its presence is what makes the two formulas above indistinguishable: the fetch itself broadcasts the pallet's location, so both are satisfied as a side effect whatever was asked for. This was checked. Adding (delivered) to all three goals and re-solving yields policies of twenty-one actions in which G1 and G2 are identical and both contain announcements the goal does not need, and the contrast collapses into which announcement is spent where. The instances here ask only who must know what, and the physical work is set by the two ontic conjuncts.
Those two conjuncts, (at-ag r2 corridor) and (at-ag r3 lane), are there so that the fleet is visibly a fleet, and they are identical in all three instances, so they cannot be what makes the policies differ. go is public ontic and reports positions, not pallets: every robot finishes the run exactly as uncertain about which aisle holds the pallet as it began. Sending r2 to the corridor and not to the lane is not arbitrary either. Parked on the lane, r2 is one move from bay 3, and the planner then discovers that the cheapest way to satisfy G3 is to let r2 look for itself: a correct plan that answers a different question. From the corridor a bay is three moves away, and being told is cheaper than going.
The semantics
The claim of this page is a semantic one and is worth stating as such before it is measured. Write \(P\) for pallet-at_bay2 and \(Q\) for pallet-at_bay3. An epistemic state is a pointed Kripke model \(\mathcal{M} = \langle W, \{\sim_i\}_{i \in \mathcal{A}}, V \rangle\) with a set of designated worlds, each \(\sim_i\) an equivalence relation, and[2, 3]
The initial state is \(\mathcal{M}_0\) with \(W_0 = \{w_2, w_3\}\), \(V(w_2) \ni P\), \(V(w_3) \ni Q\), both designated, and \(\sim_i \;=\; W_0 \times W_0\) for every agent: it is common knowledge that the pallet is in exactly one aisle, and nobody knows which.[4] In this notation the three goals of the previous section are
each conjoined with the same two ontic literals \(\mathit{at}(r_2,\textit{corridor}) \wedge \mathit{at}(r_3,\textit{lane})\), which are common knowledge throughout and play no part in what follows. \(\gamma_2\) is the only formula in this repository of modal depth two.
inspect is an event model \(\mathcal{E} = \langle E, \{\sim_i\}, \mathsf{pre}, \mathsf{post}\rangle\) with one event per outcome, both designated, and no postconditions, since looking changes what is known and not what is the case:
The observability declaration is the whole of the difference. The acting agent is Fully and everyone else is Partially, which in the action-type library are the relations
The product update \(\mathcal{M} \otimes \mathcal{E}\) has worlds[5] \(\{(w,e) : \mathcal{M},w \models \mathsf{pre}(e)\}\), valuation inherited from \(w\), and \((w,e) \sim_i (v,f) \iff w \sim_i v \text{ and } e \sim_i f\). Applying it to \(\mathcal{M}_0\) at the point where r1 stands in bay 2, exactly \((w_2,e^{+})\) and \((w_3,e^{-})\) survive, and the relations separate:
r1's relation is cut because \(e^{+} \not\sim_{r_1} e^{-}\); r2's survives because \(w_2 \sim_{r_2} w_3\) and \(e^{+} \sim_{r_2} e^{-}\) both hold. Everything else follows.
What restores \(\gamma_3\) is a public event whose precondition entails the answer. On the branch where bay 2 came back empty the actual world is \((w_3,e^{-})\), r1 knows \(Q\), and the announcement report-pallet-at_r1_bay3 is the public event with \(\mathsf{pre} = K_{r_1}Q\) and \({\sim_i} = \mathit{id}\) for every \(i\). Its product update deletes \((w_2,e^{+})\), leaving one world, and then
the first implication by the common knowledge that exactly one aisle holds the pallet. This is the step that costs the extra action, and the three and a half seconds between \(\gamma_2\) becoming true and \(\gamma_3\) becoming true in the recorded G3 run are the interval between the two updates.
The policies
Each instance is ground by plank and solved by ALETHEIA under AO*[6, 7], and the returned policy is validated by the planner's own checker against the model plank exported. The three tasks are the same size in every respect that is not the goal: 76 atoms, 198 ground actions, three agents and two designated worlds.
| Goal | Formula | Modal depth | Plan depth | Expanded | Actions | Announcement | Does the look suffice? |
|---|---|---|---|---|---|---|---|
| G1 | [Kw. r1] P | 1 | 6 | 3 952 | 6 | no | yes |
| G2 | [r2] [Kw. r1] P | 2 | 6 | 3 952 | 6 | no | yes |
| G3 | [Kw. r2] P | 1 | 7 | 8 543 | 8 | yes | no |
G1 and G2 are solved by the same six-action policy \(\pi\), expanding the same 3 952 nodes. That is the result for G2, and not a failure to find one: the deeper formula is discharged by the same sensing action that discharges the shallow one, and costs nothing beyond it. G3 is shallower and costs more.
go_r2_dock_north_corridor go_r3_corridor_dock_south go_r3_dock_south_lane go_r1_dock_south_lane go_r1_lane_bay2 inspect_r1_bay2 [semi-private] ├ e-inspect-empty => goal └ e-inspect-found => goal
go_r2_dock_north_corridor go_r3_corridor_dock_south go_r3_dock_south_lane go_r1_dock_south_lane go_r1_lane_bay2 inspect_r1_bay2 [semi-private] ├ e-inspect-empty │ report-pallet-at_r1_bay3 => goal └ e-inspect-found pickup_r1_bay2 => goal
The two policies agree on all six actions and then diverge. Every robot drives to the same place, r1 inspects the same aisle, and both branch on the same observation. G3 adds one action on each branch, and each is a public act that makes the answer available to the fleet: on the empty branch an announcement, and on the found branch the pick-up, which is public ontic and settles bay 2 by occurring. The planner was not told to prefer either. Both announcements are ground in all three instances, and G2 declines to spend one.
inspect is declared as semi-private-sensing over two events, one per outcome. The acting agent's observability is Fully, which relates each event to itself; every other agent's is Partially, which relates every event of the action to every other. So after the update r2 considers both events possible.
That is exactly the difference between the two goals, worked through in the product update above: \(\mathcal{M}_1 \models K_{r_2}\mathit{Kw}_{r_1}P\) because both events leave r1 knowing whether, and \(\mathcal{M}_1 \not\models \mathit{Kw}_{r_2}P\) because the two events disagree about \(P\) and r2 cannot tell them apart. The event model has said so since the domain was written.
plank validate reconstructs the product update itself and reports whether a given action sequence is applicable and whether the goal holds at the end. It is given the six actions the two policies share, against each goal in turn:
# the six actions G2 and G3 agree on, and nothing else $ plank validate -p nested_g1.epddl -a go_r2_dock_north_corridor … inspect_r1_bay2 true $ plank validate -p nested_g2.epddl -a go_r2_dock_north_corridor … inspect_r1_bay2 true $ plank validate -p nested_g3.epddl -a go_r2_dock_north_corridor … inspect_r1_bay2 false $ plank validate -p nested_g3.epddl -a … inspect_r1_bay2 report-pallet-at_r1_bay3 false (report-pallet-at_r1_bay3 is not applicable in 'init (X) … (X) go_r1_lane_bay2 (X) inspect_r1_bay2')
The first three lines are the result. The same trace satisfies the nested goal and the depth-one goal about r1, and fails the depth-one goal about r2. The fourth line is worth the space: appending the announcement does not repair the sequence, because the announcement is applicable on only one of the two branches. A sequence cannot be the answer to G3, and the policy that is has a different action on each branch.
The runs
Both runs are three TurtleBot3 burgers in the AWS small warehouse with the pallet standing in bay 3, launched with the same command and one argument changed. Nothing is told where the pallet is: the robots map the building with their own lasers, and plansys2_epistemic_perception classifies the region of r1's occupancy grid and reports which of the two sensing events occurred. The pallet in bay 3 is the branch worth recording, because it is the one where the first look comes back empty.
Gazebo is on the left, RViz on the right. Each robot maps separately and is drawn in its own colour, which is not decoration: the domain declares sensing semi-private, and a shared grid would quietly make every observation public and the demonstration would be proving something else. The band across the top and the three-row panel below it are burned in afterwards from the run's own log, so they cannot diverge from it. The panel is the probe's output: three formulas over one model, asked twice a second, in both runs.
| t (s) | What the log says | |
|---|---|---|
| −2 | problem seeded; asking for a plan | |
| −1 | policy: 6 nodes, 1 of them branching | |
| 0 | executing goto_zone | all three robots |
| 158 | executing look_into | |
| 158.7 | inspect_r1_bay2 observed e-inspect-empty | perception, from r1's grid |
| 158.9 | Kw_r1_P TRUE and K_r2_Kw_r1_P TRUE | both, in one probe tick |
| 158.8 | [goal] (… (K r2 (Kw r1 pallet-at_bay2))) holds | the executor's own check |
| 170 | mission complete: the policy reached its goal |
Kw_r2_P does not appear in that table, and that is the point. Across all 575 probe ticks of the G2 run it was never once true. r2 spent the run in the corridor, learned that the question had been settled, and never learned the answer, which is precisely what its goal asked for and precisely what the other goal would not accept.
| t (s) | What the log says | |
|---|---|---|
| −2 | problem seeded; asking for a plan | |
| −1 | policy: 8 nodes, 1 of them branching | two more than G2 |
| 0 | executing goto_zone | the same six drives |
| 159 | executing look_into | |
| 162.7 | inspect_r1_bay2 observed e-inspect-empty | the same observation |
| 163.1 | Kw_r1_P TRUE and K_r2_Kw_r1_P TRUE | G2's goal now holds |
| 164 | executing announce | report-pallet-at_r1_bay3 |
| 166.6 | Kw_r2_P TRUE | and only now G3's |
| 166.3 | [goal] (… (Kw r2 pallet-at_bay2)) holds | |
| 178 | mission complete: the policy reached its goal |
Between t = 163.1 and t = 166.6 of the G3 run there is a window three and a half seconds long in which G2's goal holds and G3's does not, in one execution, over one model, with one robot standing in one aisle.
The third row of the panel reads UNDECIDED and not FALSE, and the distinction is not presentational. \(\mathit{Kw}_{r_2}P\) is itself a formula, and what the state reports is that this formula fails: \(\mathcal{M}_1 \not\models \mathit{Kw}_{r_2}P\). By the definition \(\mathit{Kw}_i\varphi = K_i\varphi \vee K_i\neg\varphi\), its failure is
which says that r2 knows neither that the pallet is in bay 2 nor that it is not. It is not the claim that \(P\) is false, and it is not the claim that r2 believes anything false. The pallet is in fact in bay 3 in both runs, so \(P\) is false at the actual world throughout; r2 simply has no view on the matter, because its equivalence class after the update contains one world in which \(P\) holds and one in which it does not.
Three readings have to be kept apart, and only the panel's three states make that possible. A formula that holds; a formula that fails, which for a \(\mathit{Kw}\) formula is an open question and never an answer; and a formula the state could not be asked at all, which the probe records as no-answer and never as either of the other two.
That is the whole result, and it is visible in a frame of video. The robot has done everything it is going to do about bay 2; it has looked, and the fleet watched it look. One formula about r2 is settled by that and the other is not. Three and a half seconds later r1 says out loud which aisle the pallet is in, and the third row turns over.
The announcement on this branch is report-pallet-at_r1_bay3: r1 says where the pallet is, not where it is not. Having found bay 2 empty and it being common knowledge that the pallet is in exactly one of the two aisles, r1 knows it is in bay 3, and announcing that settles bay 2 for everyone. Either announcement would do; the planner picked one.
The instrument
The result of a nested run is not an event in the warehouse. It is an instant at which one formula over the epistemic model becomes true while another over the same model does not, and on screen that instant looks like a small robot finishing a turn. So it is measured. formula_probe is a node that dispatches nothing and is dispatched by nobody; it calls epistemic_state/check_formula every 500 ms for each of three formulas and writes what came back:
(Kw r1 pallet-at_bay2) r1 knows whether (K r2 (Kw r1 pallet-at_bay2)) r2 knows that r1 knows whether (Kw r2 pallet-at_bay2) r2 knows whether
All three are asked in both runs, whichever was the goal. That is what makes the log evidence: two of the three formulas were never the planner's goal in either run, so what the model says about them cannot have been arranged by what the planner was asked to achieve.
A formula the service could not be asked is recorded as no-answer and never as false. The whole result is that one formula is true while another is false at one instant; an unreachable service reported as false would manufacture exactly that.
This is worth stating plainly, because the opposite was the expected outcome. CheckFormula's parser is recursive over K, B, Kw, C and the connectives, and always was; render_formula on the planner's side is recursive in the same shape. The depth-one formulas the warehouse asked of them were a use of that parser, not its limit. Grounding a nested goal needed no change to plank either, which reports it as a field in the ground task:
# plank export, nested_g2.json "goal": { "modality-name": "box", "modality-index": ["r2"], "formula": { "modality-name": "Kw.box", "modality-index": ["r1"], "formula": "pallet-at_bay2" } } "planning-task-info": { …, "goal-modal-depth": 2, "goal-size": 3 }
And the executor checks the nested goal at the end of the policy through the same path, having rendered it back out of the task it was given:
[epistemic_bt] [goal] (and at-ag_r2_corridor at-ag_r3_lane
(K r2 (Kw r1 pallet-at_bay2))) holds
So the gap this page closes was never in the machinery. The domain declared semi-private sensing, the grounder accepted arbitrary modal depth, the planner searched it and the state could be asked about it. What was missing was a goal that needed any of it, and with no such goal none of it was ever exercised or shown.
Reproducing it
# ground, solve and validate the three instances cd epddl-workspace/robot-warehouse for g in g1 g2 g3; do plank export -d warehouse-domain.epddl -p instances/nested_$g.epddl \ -l intermediate.epddl -o out epistemic_planner --task out/nested_$g.json --plan out/nested_$g-plan.json \ --conditional --timeout 300 done # the comparison table, read out of what those two tools wrote python3 artifacts/nested_G2_vs_G3/table.py # the model half alone, with no simulator: walk one branch and ask # the three formulas after every step python3 artifacts/nested_G2_vs_G3/trace.py out/nested_g3.json \ go_r2_dock_north_corridor go_r3_corridor_dock_south go_r3_dock_south_lane \ go_r1_dock_south_lane go_r1_lane_bay2 \ inspect_r1_bay2@e-inspect-empty report-pallet-at_r1_bay3 # the two runs, in Gazebo, recorded and captioned artifacts/nested_G2_vs_G3/run.sh G2 artifacts/nested_G2_vs_G3/run.sh G3 # or by hand: same launch, same world, same pallet, one argument different ros2 launch warehouse_demo warehouse_demo_launch.py \ robots:=3 goal:=G2 pallet:=bay3 probe_csv:=G2.csv
Everything the two runs produced is under artifacts/nested_G2_vs_G3/: the three instances and their ground tasks, the three policies, the search logs, the full ROS logs, and the probe's CSV for both runs at 2 Hz over all three formulas.
Two things about the recording, both of which cost a run to find. The RViz configuration shipped with the demo watches /map, /scan and /robot_description, which is right for one robot and shows nothing at all for a fleet, since every one of those topics moves into a robot's namespace as soon as there is more than one; the launch now generates one set of displays per robot, each in its own colour, while the floor plan and the epistemic markers stay single because the building and the model are single. And the run script places the two windows itself, because a capture is a rectangle of somebody's desktop and ought not to depend on where the desktop last put things.
Where this leaves it
Depth. There is now a goal in the repository with an operator inside another, and it is not decorative: it is ground with goal-modal-depth: 2, searched, validated, dispatched as a policy and checked by the executor at the end of the run.
The contrast. Two goals over one world produce two policies that agree on six actions and disagree on the seventh. Since every other input is identical, the difference has one cause, and it is where the operators sit.
The semi-private sensing. The distinction the event model has always drawn (the agent that looks learns the outcome; the rest of the fleet learns that a look occurred) is now visible in a policy and in a video, because a goal finally depended on it.
The free lunch. Dropping (delivered) is what makes the two formulas separable, and adding it back collapses them, which was measured. That is a real limitation of the fetch mission as a vehicle for these questions, and it is why this page is a second demonstration and not an edit to the first.
The next instance. The three goals here range over individual modalities only. The natural continuation is the group modality: for a coalition \(G \subseteq \mathcal{A}\), the shared operator \(E_G\varphi = \bigwedge_{i \in G} K_i\varphi\) and its transitive closure
Two candidates follow directly from the present result. The first, \(\gamma_4 = C_{\{r_1,r_2\}}\,\mathit{Kw}_{r_1}P\), asks whether the fact established by the semi-private look becomes common knowledge in the pair, and is the natural strengthening of \(\gamma_2\): the inspection is observed by the whole fleet, so the question is whether observing it is enough to close the reachability closure or whether a public announcement is again required. The second, \(\gamma_5 = K_{r_3}K_{r_2}Q\), is a relay at depth two over three distinct agents, and separates “everyone was told” from “everyone knows that everyone was told”.
Both are expressible without extending anything. The C operator is in plank's grammar and in the ground-task format, the epistemic state's parser reads (C (r1 r2) φ) recursively, and the initial state of every instance on this page is already written with [C. All]. What each will cost is a question about the search: \(C_G\) is evaluated over a transitive closure and the model checking is where the expense of an extra agent already lands, which the step from 3 952 to 8 543 expansions between \(\gamma_2\) and \(\gamma_3\) only begins to indicate. That measurement is the next thing to run, and it is not on this page because it has not been.
References