Simulation · mu-calculus routing · ROS 2
A route planner asks whether a goal is reachable. This one asks a second question first: whether the cells it would drive through are known to be free, and whether the agent would be able to tell it had arrived. The two questions come apart, and a six-room building is enough to show where. Below is a single recorded run over one of the worlds in this repository, with the planner's own output at each step.
Implemented in Epistemic-Robotics, routing with mu_path_planner over 02_building_rooms.sdf.
The run
Gazebo on the left, RViz on the right. The map RViz draws is the one the planner is given: white where the occupancy grid reports free, teal where nobody has observed anything yet. Green is the route the fixed point returns, blue the polyline the base actually drives, red the cells where sensing would pay.
The steps are chosen to separate the two questions and not to show a robot getting somewhere:
| Step | What it asks | What comes back |
|---|---|---|
| 1–2 | Ontic goals: room 2, then room 5 | Routes, driven |
| 3 | The target, lying in rooms nobody observed | No route. Unknown is not free |
| 4–5 | Room 3 sensed; the same query again | A route, because the cells became free |
| 6–7 | An epistemic goal over a disputed target | Sensing waypoints, not a route |
| 8–9 | The observation collapses the model | One world left: it knows, and goes |
What the planner said
Every query in the run is logged with the sets the fixed point was taken over. Three lines carry the whole argument, and they differ only in what was known when they were asked:
# nobody has looked into the room the target lies in zone='target' epistemic=0: goal=0 known=0 disputed=804 region=0 path=0 # the same query, after a sensing action resolves that room zone='target' epistemic=0: goal=356 known=0 disputed=804 region=24907 path=113 # asking to *know* it arrived, once the model has collapsed to one world zone='target' epistemic=1: goal=356 known=356 disputed=0 region=30167 path=107
The first is asked while the target's room has never been observed. goal=0: not one cell of the zone is known free, so the least fixed point halts with an empty winning region and there is no route, in a building whose corridors are entirely open. Nothing was blocking the robot except that it had not looked.
The second is the same query after a sensing action resolves the room. The zone did not move and the walls did not change; 356 cells became known free, and a 113-cell route appears.
The third asks for knowledge, not arrival. Between the two worlds the agent holds possible the target lies in different rooms, so while disputed=804 the agent cannot come to know it has arrived, however easily it can stand on the cell, and what comes back is where to sense, not where to drive. Only once the observation collapses the model to a single world does known catch up with goal, and the route follow.
The fixed point
The three log lines above differ in the sets the fixed point was taken over, and those sets are what the planner computes. Let \(C\) be the cells of the grid and let \(R \subseteq C \times C\) relate a cell to the cells a step can reach from it. Write \(\mathit{Free}\) for the cells observed and settled free, \(\mathit{Goal}\) for the cells of the queried zone that are in \(\mathit{Free}\), and take the least fixed point[1]
This is the smallest set containing the goal cells and closed under taking a free predecessor. A route exists exactly when the robot's own cell lies in it. The operator is monotone in \(X\) over the powerset lattice of \(C\)[1, 2], so the fixed point exists and the iteration terminates; the planner's region figure is its cardinality.
The first query answers \(\mathit{Goal} = \emptyset\), and the least fixed point of an operator whose base case is empty is empty:
Nothing is unreachable in the building; the set the iteration would have grown from does not exist yet. This is the whole content of goal=0 … path=0 in a building whose corridors are open, and it is why the honest answer to the first query is that no route is known to exist. Treating unobserved cells as free would replace \(\mathit{Free}\) with \(C \setminus \mathit{Occupied}\) and return a route across floor nobody has measured.
The third query asks something the first two do not. Let \(W\) be the worlds the agent holds possible and \(\mathit{Goal}_w\) the goal cells in world \(w\). Arrival is a fact about one world; knowing one has arrived is a fact about all of them, so the target set is the intersection
With disputed=804 the two worlds place the target in different rooms, the intersection is empty, and by the argument above the winning region is empty as well. No amount of driving changes that, because driving does not change \(W\). What the planner returns instead is a cell from which a sensing action would collapse \(W\), which is why the answer to a query about knowledge is a place to look and not a place to stand.
Driving it
The fixed point returns a path over a 4-connected grid, which is a staircase grazing every inside corner: not something a differential base can drive. Three layers sit between it and the wheels. Line-of-sight shortcutting removes the corners that can be seen past; a smoother pulls what remains towards a curve, undoing any step that would put a point somewhere the map does not call free; and a dynamic window samples the velocities one acceleration step away, rolls each forward as an arc, and scores the survivors on progress, clearance and speed. The laser has the final say, so an obstacle the map never had is still avoided.
Measured against Gazebo's own poses for the robot and not against its odometry: wheel odometry keeps integrating while a base is held against a wall, and so cannot answer this question at all:
| Distance driven | 24.71 m |
| Closest approach to any obstacle | 0.225 m |
| Robot body radius | 0.105 m |
| Contacts | 0 |
Reproducing it
The harness lives in demo/ and is deliberately outside the ROS packages, so that nothing in them depends on it. It rasterises the world SDF into the occupancy grid the planner subscribes to, publishes a Kripke snapshot grounding the six rooms as zones, and walks the script.
colcon build && source install/setup.bash ./demo/run_demo.sh out.mp4 # gazebo and rviz side by side, recorded REHEARSE=1 ./demo/run_demo.sh # the same, without recording ./demo/smoke.sh # headless, for checking the logic alone
Both controllers run on /clock. The GUI does not simulate at wall-clock speed, and a controller ticking on wall time issues several commands per simulated step: the window opens faster than the base can accelerate, and the robot overshoots into whatever it was rounding.
References