An epistemic policy on a floor RMF was never given
The warehouse mission of robot-warehouse
was executed over an Open-RMF fleet in the AWS RoboMaker small warehouse,
a world with no traffic-editor description and no RMF assets of its own.
The navigation graph and the building map were derived from the same
constants the rest of the repository reads its floor plan from, and both
were validated against the occupancy grid before use. The run completed in
nine actions with no traffic negotiation failures, and every agent's
accessibility relation remained reflexive throughout.
Domain and instance from
epddl-workspace/robot-warehouse, unmodified.
Planned by Aletheia,
executed by eplansys,
dispatched by eplansys-rmf.
The problem
Two aisles and a pallet
A pallet stands in one of two aisles, bay2
and bay3. Its location is settled and
unknown to the fleet, so the initial model has two worlds and designates
both. Two agents participate: r1, which
comes on shift at shipping, and r2, which
waits at receiving and never moves.
The first conjunct is ontic. The second requires the stationary agent to
come to know which aisle held the pallet. The pickup action carries a
modal precondition,
([?i] (pallet-at ?z)), so a robot may
lift the pallet only where it knows the pallet to be, and any plan that
satisfies the goal contains an inspection.
Inspection is semi-private-sensing: the
fleet observes that an aisle was inspected and does not observe the
result. Movement and pickup are public-ontic.
The domain also supplies a public announcement, which the policy for this
instance leaves unused for reasons the measurement below makes clear.
The environment
Deriving an RMF world from a floor plan
Open-RMF obtains its navigation graph from a traffic-editor
.building.yaml, which also generates the
Gazebo world. The AWS small warehouse exists already and has no such
description, so both artefacts were generated in the world's own metres
from the constants in
warehouse_scenario/include/warehouse_scenario/warehouse.hpp.
The zones RMF routes between are then the zones the μ-calculus planner
routes over.
The building map is required even though the warehouse has one level, no
doors and no lifts. The slotcar plugin queries the building map server for
the level a robot occupies, and it publishes no robot state without an
answer, so an absent map leaves RMF with no fleet at all.
Figure 1. The navigation graph over the warehouse floor. Circles
ringed in red are zones the epistemic domain names; smaller circles are
corners the route requires and the domain does not mention. The dashed
line is a lane the validator refuses.
Validating the graph against the floor
A first version of the graph ran a lane east along the south wall, joining
dock_south to the service lane by the
shortest path on the plan. That lane crosses the rack block. The
consequence in simulation was quiet: RMF accepted the task, the robot
drove to within 0.75 m of the shelving, which is its configured
stop_radius, and stopped. The task neither
completed nor failed, and the bridge waited until its timeout.
The graph generator now takes the occupancy grid as an argument and
refuses to emit a graph whose waypoints or lanes intersect occupied floor.
A scan for east–west corridors clear over the whole span from the
west corridor to the service lane returns two bands, at
\(y = -8.9\) and \(y \in [-5.6,\, 0.9]\); the crossing is placed at
\(y = -5.0\), inside the wider one.
A second constraint was added after a second failure. Each robot claims a
vicinity radius of 0.5 m in addition to its footprint, so two robots
require about a metre between their centres. With
r2 parked on
dock_north, which is where
r1 delivers, RMF logged
Failed negotiation 102 times over four
minutes and never failed the task. The generator now requires 1.4 m
between every parking spot and every zone.
A zone in the epistemic domain is a region several agents occupy at once,
and a waypoint in RMF admits one robot. Both statements about
r2 are true simultaneously: the model
places it in zone dock_north and the fleet
parks it 1.5 m away.
Execution
The run
Aletheia solved the instance by AO* at depth 11, expanding
1 448 279 nodes and generating 1 459 711. The
executor rendered a policy of seventeen nodes. Nine actions were dispatched
before the goal held, over 172.5 s of wall-clock time, with no
negotiation failures.
Figure 2. The policy, drawn from the plan the planner emitted. A
conditional plan is an AND–OR tree: an action, and one continuation
per event that action can produce. The single branch point is the
inspection, whose two events divide a six-node continuation from an
eleven-node one. The branch the recorded run took is drawn in full; the
counterfactual is greyed. The red outline marks the sensing action and
the black outlines the two that change the world.
Figure 3. The recorded run, with the pallet in aisle 2. Gazebo on
the left, the RMF schedule view on the right; r1 drives, r2 stays on its
charger and comes to know which aisle held the pallet anyway. Recorded on
a display of its own; sped up three times, with captions generated from
the run's log. This is a separate execution of the same instance from the
one measured below, recorded with both interfaces drawing in software.
step
action
execution
|W|
|D| r1
|D| r2
0
initial state
–
2
2
2
1
go dock_south → lane
40.7 s
2
2
2
2
go lane → bay2
15.3 s
2
2
2
3
inspect bay2
6.0 s
2
1
2
4
pickup bay2
6.0 s
1
1
1
5
go bay2 → lane
16.0 s
1
1
1
6
go lane → dock_south
39.5 s
1
1
1
7
go dock_south → corridor
20.5 s
1
1
1
8
go corridor → dock_north
19.5 s
1
1
1
9
unload dock_north
6.0 s
1
1
1
Motion accounts for 151.5 s of the 172.5 s. The inspection that
settles the mission's uncertainty occupies six seconds, and the aisle it
enters was reached in the preceding 56.
Measurement
Information gain over the run
The run was replayed against a standalone epistemic state and each agent's
perspective was measured after every action.
Figure 4. The measured run. No cell is marked in red: every
perspective contains the actual world at every step.
The model contracts. It has two worlds until step 4 and one thereafter,
and the transition occurs at the pickup. Uncertainty is resolved twice and
by two different mechanisms. At step 3 the inspection settles the aisle for
r1 alone, which is what semi-private
sensing provides: the other agent observes that an inspection occurred. At
step 4 the pickup settles it for both, because a public ontic action whose
precondition names the aisle discloses the aisle to every observer.
The goal is a formula of the modal language, and what the semantics
assigns it is not a truth value but an extension,
\([\![\varphi]\!]^{\mathcal{M}} = \{w \in W : \mathcal{M}, w
\models \varphi\}\), with satisfaction the containment \(W^{*}
\subseteq [\![\gamma]\!]\). The extensions below are computed by the
labelling algorithm on the models the run recorded, and reproduce every
verdict the executor reported.
The extension of each subformula of the goal, after every action\(\gamma \equiv \texttt{delivered} \wedge \mathit{Kw}_{\texttt{r2}}\,\texttt{pallet-at}\_\texttt{bay2}\)
A dot is a world of that step’s model, filled where the formula holds and ringed where the world is designated. The goal is satisfied exactly where every ringed dot in the bottom row is filled, which is the containment \(W^{*} \subseteq [\![\gamma]\!]\).
The model contracts, so the extensions contract with it, and after step 4
every formula is decided by a single world. One row repays attention:
\([\![\texttt{pallet-at}\_\texttt{bay2}]\!]\) is empty from step 4
onwards, because the pick-up removes the atom, while
\([\![\mathit{Kw}_{\texttt{r2}}\,\texttt{pallet-at}
\_\texttt{bay2}]\!]\) becomes the whole model at the same step. Knowing
whether survives the proposition ceasing to hold: what
r2 comes to know at the pick-up is that
the aisle is settled, and the settlement outlives the pallet's being
there.
The same question as a refutation
The goal test also reduces to propositional satisfiability. One variable
\(x_{\psi,w}\) per subformula and world, the defining clauses of each
connective and each modality, and \(\neg x_{\gamma,w}\) asserted at the
designated world; the encoding is unsatisfiable exactly when the goal
holds.
The goal test on the final model, as a propositional refutation7 variables, 15 clauses
\(\neg x_{\gamma,w} \ \text{ for each } w \in W^{*}\)
1
unsatisfiable · 7 unit propagations, 0 decisions · \(\gamma\) is entailed at every designated world, so the goal holds.
The same question decided as a propositional refutation. Every recorded verdict of the run is reproduced by both procedures.
The valuation enters as unit clauses, so unit propagation closes the
instance without a single decision. Both procedures agree with each other
and with the run at all ten steps.
The second goal conjunct is satisfied at step 4 by an agent that never
moved and never communicated. This accounts for the absence of the
announcement from the policy: the public pickup already discloses what an
announcement would say, and the planner spends no action on it. A third
agent, or an instance in which the inspection returns an empty aisle,
changes that, and the three-robot instances in
robot-warehouse measure the difference.
Figure 5. The same relations counted as graphs. The preceding
table counts vertices; this counts edges and checks the closure
properties they satisfy. r1 loses two edges at the inspection while r2
keeps all four, which is the semi-private sensing: one agent separates
the worlds and the other does not. Both fall to a single reflexive edge
at the pickup. Every cell reports S5, so the properties were satisfied
at every step of the run.
Figure 6. Each agent's accessibility relation, stepped through the
run. Every world keeps its self-loop at every step, which is the
\(\mathrm{S5}_n\) condition holding throughout.
Every relation in this run is reflexive at every step, so the frame is
\(\mathrm{S5}_n\) from beginning to end and no agent holds a belief the
world contradicts. Every action here is public or semi-private, and the
information available to an agent grows monotonically. The
hotel incident admits private ontic change and
private announcement, and its measurement shows both the model growing and
two agents ending outside the actual world.
The argument selects the aisle the pallet occupies, and the two values
drive the policy down its two branches. The world is the AWS RoboMaker
small warehouse, launched unmodified, with RMF's robots spawned into it.
The graph generator exits with an error listing every waypoint and lane
that intersects occupied floor, and every parking spot closer to a zone
than two robots can stand. The building map is derived from the graph, so
the two cannot disagree.
