Gazebo · EPDDL · ePlanSys · Nav2
The RoboticsAcademy multi-robot Amazon warehouse exercise supplies a fleet, a floor of racks, a pallet and a dock, and asks for a task planner that assigns the jobs. The pallet's location is given to that planner as part of the problem statement. This page states the same mission with the assumption removed: the pallet stands in one of two aisles and no robot knows which. Under that formulation no action sequence solves the problem, since each sequence fixes an aisle in advance and is unexecutable in the world where the pallet is in the other. The solution is a conditional policy whose branch is selected during execution by a sensing action.
The floor is the one used by the original exercise: AWS RoboMaker's small warehouse, at its own coordinates. Domain in epddl-workspace/robot-warehouse, execution in ros2_ws/src/warehouse_demo, both in Epistemic-Robotics. Full report (PDF)
The run
Gazebo is on the left, RViz on the right. The occupancy grid RViz displays is produced by slam_toolbox from the robot's own laser during the run: white marks cells measured free, teal marks cells not yet observed. The caption band is composed from the run's log, using the actions ePlanSys dispatched and the timestamp at which the epistemic state changed, and is burned in afterwards with ffmpeg; it therefore cannot diverge from the recorded execution. The status in the upper right is the result of an EpistemicStateClient::check_formula query issued during the run, and reports UNKNOWN until the sensing action completes.
Timings from the run's own log, relative to the first action dispatched:
| t (s) | What the log says | |
|---|---|---|
| −2 | problem seeded; asking for a plan | |
| −1 | policy: 17 nodes, 1 of them branching | |
| 0 | executing goto_zone | shipping → lane → bay 2 |
| 79 | executing look_into | |
| 79.2 | (Kw r1 pallet-at_bay2) holds after 0.4s | the model settles |
| 80 | executing pick_up | now permitted |
| 84 | executing goto_zone | bay 2 → ⋯ → receiving |
| 212 | executing drop_off | |
| 227 | mission complete: the policy reached its goal |
This execution followed the found branch: the pallet was in bay 2, so the policy proceeded directly from the sensing action to the pick-up. Had the bay been empty, the alternative branch adds three moves, since the zone graph contains no edge between the two aisles and the robot must return to the service lane before entering the other.
The fleet
The execution above follows the shorter of the two branches: r1 inspects bay 2, the pallet is present, and it is lifted. That trace is observationally indistinguishable from a fixed sequence, so it does not by itself demonstrate that the plan is conditional. The caption states the branch structure; the robot does not exhibit it.
The following execution is the same mission with the pallet placed in the other aisle. The domain, the instance and the goal are unchanged, and no component is informed of the change: the only difference is the spawn coordinate passed to Gazebo, which is a fact about the world and not about the planning problem.
Two behaviours occur on this branch that cannot occur on the other. The first is the return to the lane. The rack rows terminate 0.15 m short of the east wall, which is impassable to a robot 0.21 m across, so the zone graph contains no edge between the two aisles and an incorrect first inspection costs three additional moves. That cost belongs to the building, not to the encoding.
The second is the announcement. In the two-agent instance the planner selects no announcement, because pickup is a public ontic action: observing r1 remove the pallet from a bay is sufficient for r2 to determine which bay held it. In the three-agent instance on this branch that inference is unavailable. The goal conjunct concerns pallet-at_bay2, and observing a pick-up in bay 3 settles only bay 3; the fact that establishes the conjunct is r1's failure to find the pallet in bay 2, which is not a public event. The planner therefore spends report-pallet-at_r1_bay3:
[epistemic_perception_r1] 'bay2' is clear: inspect_r1_bay2 observed e-inspect-empty [look_action_r1] (Kw r1 pallet-at_bay2) holds after 0.8s [epistemic_bt] [(look_into r1 bay2)] observed e-inspect-empty [announce_action_r1] radioing the fleet at bay3 [warehouse_mission] executing announce ... [warehouse_mission] mission complete: the policy reached its goal
The epistemic status becomes [Kw. r1] pallet-at_bay2 = TRUE at the moment the bay is observed empty. This is correct: Kw is the knowing-whether modality, which is satisfied by determining that the proposition is false as much as by determining that it is true.
In this instance the goal conjunct is [Kw. r2] pallet-at_bay2, yet r2 remains at receiving for the entire run and issues no action; the log contains no action lines for it. The conjunct is established by the public effect of r1's pick-up. The planner selects this without any preference for it being encoded in the domain: a solution in which r2 travels to a bay and inspects it also satisfies the goal, and is longer.
| Run | Policy | Branch taken | Announcement | Robots that move |
|---|---|---|---|---|
| 1 robot | 17 nodes | found | – | r1 |
| 2 robots | 17 nodes | found | none needed | r1 |
| 3 robots | 21 nodes | found | none needed | r1, r3 |
| 3 robots, pallet moved | 21 nodes | empty | r1 radios bay 3 | r1, r3 |
What is actually running
The system comprises one planning layer for the fleet, one set of action nodes per robot, and one navigation stack per robot in a namespace of its own. The placement of each node relative to that namespace boundary is determined by whether it operates on fleet-wide state or on a single robot's observations, and in three cases below the placement is forced.
Each robot maintains its own map. Every mapper publishes to that robot's /rN/map, and each perception node subscribes only to the map of the robot it reports for. The cost is one SLAM instance per robot. Consolidating them would be cheaper and unsound: the domain declares looking as semi-private sensing, under which the observing agent learns the outcome and the others learn only that an inspection occurred. A shared grid makes every observation available to every agent, which is public sensing, and the execution would then no longer correspond to the domain being solved. The separation also has to be made explicitly, because slam_toolbox names its services relative to the node and its map topic absolutely: three mappers in three namespaces publish to the same /map until that topic is remapped.
The action nodes are not namespaced. PlanSys2's ActionExecutorClient advertises actions_hub under a relative name, so a node placed in a robot's namespace would advertise a separate hub and never receive the fleet's dispatches. The action nodes therefore run in the global namespace, one set per robot, and are distinguished by specialized_arguments, which the executor matches positionally against the arguments of the action being dispatched. Every topic that belongs to a particular robot is remapped into that robot's namespace individually.
The building is shared; the measurement is not. Nav2 plans over /floorplan, the rasterised AWS world, served once for the whole fleet. This models the fact that a warehouse robot is issued the building's layout. It is not issued a record of which parts of that layout it has observed, and that record is the per-robot /rN/map over which the µ-calculus planner computes reachability and from which perception derives its observations.
The domain
The domain declares six zones: shipping and receiving at the two ends of the west corridor, the service lane along the rack fronts, and the two candidate aisles opening off it. Driving, lifting and unloading are public ontic actions, on the grounds that a warehouse fleet tracks the positions of its own members. Looking is semi-private sensing. The pick-up event carries a conjunct that constrains the agent's information, not the state of the warehouse:
(:event e-pickup :parameters (?i - agent ?z - zone) :precondition (and (at-ag ?i ?z) (bay ?z) (pallet-at ?z) ([?i] (pallet-at ?z)) (not (carrying ?i))) :effects (:and (carrying ?i) (not (pallet-at ?z))))
(pallet-at ?z) is a proposition about the warehouse; ([?i] (pallet-at ?z)) is a proposition about the agent's knowledge. The first makes the lift physically possible, the second makes it applicable. Removing the second conjunct recovers the classical domain exactly: a robot standing in the correct aisle may then lift a pallet it has no grounds to believe is present, and a plan containing no sensing action becomes valid. The following rejection is produced by plank validate:
# plank validate -a go_r1_dock_south_lane go_r1_lane_bay2 pickup_r1_bay2
false (pickup_r1_bay2 is not applicable in
'init (X) go_r1_dock_south_lane (X) go_r1_lane_bay2')
Looking is declared as semi-private sensing with one event per outcome and a <Kw. ?i> conjunct in both preconditions. The observing agent learns the outcome; any other agent present learns that an inspection occurred but not its result; and an inspection of a proposition the agent has already settled is inapplicable, not merely redundant. With a single agent this declaration has no observable effect, since there is no second agent whose information could differ. It is retained because the effect appears as soon as a second agent is added, and the one- and multi-agent instances share a domain.
The two events have contradictory preconditions and neither is entailed by the initial model, so at plan time it is undetermined which will occur. This is the property that makes the solution a policy:
go_r1_dock_south_lane [public-ontic] go_r1_lane_bay2 [public-ontic] inspect_r1_bay2 [semi-private-sensing] +-- e-inspect-empty (not pallet-at_bay2) go_r1_bay2_lane, go_r1_lane_bay3, pickup_r1_bay3, go_r1_bay3_lane, go_r1_lane_dock_south, go_r1_dock_south_corridor, go_r1_corridor_dock_north, unload_r1_dock_north => goal reached +-- e-inspect-found (pallet-at_bay2) pickup_r1_bay2, go_r1_bay2_lane, go_r1_lane_dock_south, go_r1_dock_south_corridor, go_r1_corridor_dock_north, unload_r1_dock_north => goal reached
The product update along this policy is reconstructed independently of the planner, from the model plank exported and the events it ground, and is checked at every node: each action must be applicable in the model reached at that point, and the goal must hold at every leaf. tools/show_plan.py performs this check and exits non-zero if the reconstruction and the planner disagree.
The semantics
The informal claim above, that each action sequence fixes an aisle in advance and is unexecutable in the world where the pallet is in the other, is a statement about a model, and it is worth writing down as one. Let \(P\) abbreviate pallet-at_bay2 and \(Q\) abbreviate pallet-at_bay3. An epistemic state is a Kripke model \(\mathcal{M} = \langle W, \{\sim_i\}_{i\in\mathcal{A}}, V \rangle\) with a set \(W_d \subseteq W\) of designated worlds, each \(\sim_i\) an equivalence relation, and[1, 2]
The instance designates two worlds, \(W_d = W = \{w_2,w_3\}\) with \(P\) true at \(w_2\) and \(Q\) true at \(w_3\), and every agent's relation is all of \(W \times W\): it is common knowledge that the pallet is in exactly one aisle, and it is common knowledge that nobody knows which. The goal of the two-agent instance is
A solution is a policy \(\pi\)[3], and it must reach \(\gamma\) from every designated world. The pick-up event carries
and an event is applicable in \(\mathcal{M}\) only when its precondition holds at every designated world. Before any sensing, \(\mathcal{M}_0 \not\models K_{r_1}P\) (\(w_3 \sim_{r_1} w_2\) and \(P\) fails at \(w_3\)), so \(\textsf{e-pickup}_{r_1,\textit{bay2}}\) is inapplicable at the initial state no matter where r1 is standing. Dropping the underbraced conjunct recovers the classical domain, in which applicability is a question about the warehouse alone and a plan that never inspects anything is valid.
What makes the pick-up applicable is the product update at the inspection. inspect is an event model with one event per outcome and no postconditions,
and \(\mathcal{M}\otimes\mathcal{E}\) keeps the pairs[4] \((w,e)\) whose precondition holds, with \((w,e)\sim_i(v,f)\) exactly when \(w \sim_i v\) and \(e \sim_i f\). The acting agent's event relation is the identity, so \((w_2,e^{+}) \not\sim_{r_1} (w_3,e^{-})\): r1's classes become singletons and \(K_{r_1}P\) holds in one of them. The update also splits the designated set in two, and a plan whose next action was chosen before the split is applicable in only one half. That is the formal content of “the plan is a policy”.
The floor
The grid is rasterised from the collision meshes Gazebo loads for that world (the building shell, six rack rows, the tall shelf on the west wall and the clutter between them), sampled at the heights at which a ground robot can strike them. It is therefore the same geometry the laser measures at run time, and the two cannot diverge. The two occupancy grids AWS distributes with the world were not used: both are SLAM captures, are sparse, and omit most of the rack structure, which would make every result contingent on the trajectory driven when they were recorded.
The rack rows terminate 0.15 m short of the east wall. A planner treating the robot as a point admits that gap as a corridor running the length of the rack block and connecting every aisle to every other; the resulting routes are not drivable by a TurtleBot3 burger, which is 0.21 m across. Inflating the obstacles by the robot's 0.105 m radius closes the gap and leaves 0.7 m of clearance in each aisle. In the zone graph each aisle is consequently a pocket with a single mouth on the service lane, there is no edge between bay 2 and bay 3, and an incorrect first inspection costs three moves. This follows from the geometry of the world, and not from a simplification of it.
| Grid | 281 × 421 cells at 0.05 m |
| Building | 14 m × 21 m |
| Robot body radius | 0.105 m |
| Gap behind the racks | 0.15 m: open on the plan, shut on the planner's grid |
Crossing it
The robot begins at shipping with an empty occupancy grid. The service lane is not occupied; it is unobserved, and the µ-calculus planner excludes unobserved cells from the least fixed point instead of treating them as free. Early in a run the correct answer to a query for a route to the lane is therefore that no route is known to exist, and the planner returns that:
to lane: at (-3.50, -9.30), asked 'lane', 0 legs; 0 cells of lane measured so far no route to lane yet; going to look from (-1.96, -9.28) to lane: at (-1.76, -9.03), asked 'lane', 15 legs, and the zone is not on the map yet to lane: at (0.36, -8.83), asked 'frontier', 24 legs; 285 cells of lane measured
When the destination is unreachable the drive action selects a frontier: a cell that is known free, admits the robot and the planner's inflation radius, and has unobserved cells within sensor range. It requests a route to that cell instead, drives it, and re-issues the original query against the enlarged map. Three properties of the selection are required for termination, and each was established by a run that failed without it. The target must border unobserved space, or the map ceases to grow and the destination remains unreachable. The score must credit distance travelled, or the robot advances a short distance toward the blockage and re-selects the same region. And a selected frontier must be retained until it is reached, since arriving at one clears the no-route condition, which causes the next cycle to query the destination, fail, and select a different frontier indefinitely.
None of this selection is epistemic. It is the mechanism by which the robot acquires the map that the route planner and perception subsequently reason over. The determination of what was observed is made elsewhere: look_into orients the robot toward the bay, holds it there, and terminates when the epistemic state reports that the corresponding knowledge formula holds. That formula is established by plansys2_epistemic_perception, which classifies the configured region of the occupancy grid and reports which of the two sensing events occurred. The action node does not determine the outcome, which is what distinguishes the observation from a scripted one.
Scaling
The two-agent instance assigns the epistemic conjunct to the robot that remains at receiving; the three-agent instance assigns it to two robots, neither of which performs the inspection. The mission itself does not become harder: the plan has the same structure and r1 performs the same physical work in each case. The search does, and the figures below are produced by validate.sh.
| Agents | Atoms | Ground actions | Worlds | Depth | Expanded | Generated | Seconds |
|---|---|---|---|---|---|---|---|
| 1 | 62 | 66 | 2 | 11 | 1 008 | 1 012 | 0.01 |
| 2 | 69 | 132 | 2 | 11 | 18 254 | 18 525 | 0.23 |
| 3 | 76 | 198 | 2 | 12 | 195 178 | 197 533 | 2.90 |
Expansions grow by roughly an order of magnitude per agent (×18, then ×11) while the number of worlds is unchanged at two. Each additional agent contributes a further accessibility relation over those worlds, and evaluating a formula about any agent's knowledge requires checking every relation, so the growth is in the model checking, not in the size of the state space.
The two-agent policy contains no announcement, although the domain declares report-pallet-at and it is ground in every instance. None is required: pickup is a public ontic action, so r2 observing r1 remove the pallet from a bay is sufficient to establish which bay held it. In the three-agent instance the planner does select one, inserting report-pallet-at_r1_bay3 on the branch where bay 2 was found empty. On that branch the goal conjunct concerns bay 2 and is established by the absence of the pallet there, which produces no public event; the pick-up that follows occurs in bay 3 and settles bay 3 only.
This behaviour was not encoded in the domain. Both announcement actions are available in every instance, and the difference between the policies is a result of the search.
Reproducing it
# one, two and three agents; the two rejections; the scaling table bash epddl-workspace/robot-warehouse/validate.sh # the floor, and the six route-planning cases, offline and over ROS colcon build --packages-select epistemic_msgs mu_path_planner warehouse_scenario bash scenarios/warehouse/run_demo.sh colcon test --packages-select warehouse_scenario # 12 tests # the full system in Gazebo ros2 launch warehouse_demo warehouse_demo_launch.py
A bay becomes visible from the service lane thirty to sixty seconds before the robot reaches it, and the epistemic state rejects an observation from a robot it does not yet hold to be in that bay. Perception therefore re-offers the reading until the executor has applied the preceding drive, bounded by applicability_retries, set here to 240. The default of 40 grid updates is a few seconds, which is appropriate to a building of small rooms and not to a warehouse aisle.
References