Domain
building-rooms · a six-room floor
Six rooms and the doors between them, with an occupancy grid a robot measures as it goes. Movement is public-ontic and looking is semi-private-sensing. The frame is \(\mathrm{S5}_n\). Two runs use it: one asks what routing over a partially measured floor costs, and one states a mission whose goal is a modal formula.
The six-room run
Nine queries put to a μ-calculus route planner, separating reachability from the question of whether the agent could tell it had arrived. Cells nobody has observed are excluded from the fixed point, so the least fixed point halts at the mouth of an unmeasured corridor.
The six-room survey
The same building with a goal stated in EPDDL. The plan is a policy, and the branch is taken on what the robot observes.
Domain
robot-warehouse · the AWS small warehouse
The RoboticsAcademy multi-robot Amazon warehouse exercise in its epistemic reading. A pallet stands in one of two aisles, nobody is told which, and pickup carries the modal precondition ([?i] (pallet-at ?z)), so a robot may lift it only where it knows it to be. Inspection is semi-private and every other action is public, which keeps the frame \(\mathrm{S5}_n\). Three runs use it, differing in the goal, the fleet size, and the layer driving the robots. Two further entries below share the setting and not the domain: Epistemic planning on a warehouse floor at scale executes the survey domain of the six-room demos on a warehouse floor and evaluates that execution at scale, and Knowing which, and knowing about a place nobody went gives that domain's contamination a location, which is what makes the floor and the epistemics meet.
The warehouse run
The mission executed for one robot, then two, then three, under Nav2. The third robot is where an announcement starts earning its place: watching a pickup settles the aisle, and watching an empty aisle settles nothing.
Nested epistemic goals
Three instances identical except for the modal depth of the goal. Second-order knowledge is sometimes free and sometimes costs an announcement, and the difference appears in the search before it appears in the plan.
The warehouse over Open-RMF
The same domain executed by an RMF fleet in a world with no traffic-editor description of its own. The navigation graph and building map are derived from the floor plan and validated against the occupancy grid before use. Every relation stays reflexive and the model contracts from two worlds to one.
Epistemic planning on a warehouse floor at scale
The survey domain, not this one, on a derived 42 × 63 m floor. Graph recovery and a scan that costs metres, not a larger policy: the plan is the same four nodes it is on the small floor. The outcome it branches on is read off the robot's laser, and the same binary takes different branches in two worlds differing by one pallet. Execution of an epistemic policy at scale, and the eight defects that finding it turned up.
Knowing which, and knowing about a place nobody went
The same floor, corrected, and a domain in which contamination has a location: exactly one of three sites, and nobody knows which. One line of EPDDL takes the search from 40 expansions to 838 168 and the policy from four nodes to eight, and sends two robots to two aisles. Down one leaf the team ends up knowing the state of a site no robot approached and no laser was pointed at. Three worlds, three leaves, and the floor the previous page measured turns out to have been the wrong one.
A link that actually falls
SLAM answers where the robot is and what the building looks like; it does not answer who knows that. Every other demonstration keeps the grid and the knowledge model as two views of one fact. This one cuts the radio between two robots and takes that coincidence away. The cut has no appearance in the simulator, so what the film watches is the belief: an arrow where one robot thinks the other is, and a disc the size of how far it has drifted from being knowledge.
Domain
pass-through · three bays in a racking block
Exactly one of three pass-through bays is open, and which one is common knowledge only as a disjunction. Surveys are semi-private sensing read off each scout's own SLAM map; map exchanges are semi-private announcements carried by map fusion; and cross carries the precondition \(K_{\mathit{carrier}}\,\mathit{open}(t)\), which the carrier's route enforces as a least fixed point over what it knows. The frame stays \(\mathrm{S5}_n\). One run so far, and all three worlds validated.
A route through a bay no map contains
Two scouts find loads in two bays, and the carrier crosses the third, which no robot surveyed and of which the two map exchanges carried not one cell. The scouts know it is open only jointly; the exchanges make it the carrier's, and the safe set of its route lifts the bay into the fixed point on that knowledge alone.
Domain
hotel-incident · three floors and two lifts
A leak in one of two suites on separate floors. The domain admits private-ontic change and quasi-private-announcement, so an agent that observes neither continues to hold what it last had reason to hold. The reachable frame is therefore \(\mathrm{KD45}_n\), and the transition out of \(\mathrm{S5}_n\) happens during execution. One run uses it so far.
The hotel incident
Two robots dispatched to different floors by a single joint action, and a containment only the suite observes. The agents' knowledge is measured after every action: two of the three end holding beliefs the world contradicts, and each of those is attributable to one action.