EPDDL · ePlanSys · DEL policies on ROS 2
The companion page on this site routes a robot with a mu-calculus fixed point. This one asks a different question of the same building. The mission is to come to know whether the east wing is passable, which the robot satisfies without entering it. The mission is written in EPDDL, and the answer is supplied by a map the robot builds with its own laser and not by anything the planner imagines.
Domain and instance in epddl-workspace/building-rooms; executed on ePlanSys, grounded with plank, solved by Aletheia. Technical report (PDF)
The run
Gazebo on the left, RViz on the right. The map RViz draws is the one the robot is building as it drives, and the captions name the mission's goal, the epistemic action running at that moment, and how far through the policy the executor has got.
What to watch for: the robot drives into room 3, turns to face it, and holds still. The caption changes from ONTIC goto-door3_r1 to SENSING inspect3_r1, and a moment later the map fills in and the region resolves. That observation is what the policy branches on, and only then does the robot set off for room 6.
[planner] [epistemic] policy with 6 nodes, branching [perception] 'room3' is blocked: inspect3_r1 observed e-inspect3-blocked [epistemic] applied inspect3_r1 -> e-inspect3-blocked [bt] (look_into r1 door3) observed e-inspect3-blocked [epistemic] applied goto-door6_r1 [perception] 'room6' is clear: inspect6_r1 observed e-inspect6-clear [bt] (look_into r1 door6) observed e-inspect6-clear [bt] [goal] (and (Kw r1 blocked-r3) (Kw r1 blocked-r6)) Successfully finished
The two rooms answer differently, which is the point: the branch is exercised and not merely implied. Nothing in the stack decided those answers both came from the occupancy grid the robot built with its own laser.
| Distance driven | 27.88 m |
| Closest approach to any obstacle | 0.307 m |
| Robot body radius | 0.105 m |
| Contacts | 0 |
Measured against Gazebo's own poses for the robot, not its odometry: wheel odometry keeps integrating while a base is held against a wall, so it cannot answer whether anything was hit.
The domain
Rooms 3 and 6 lie east of the cross corridor; the robot starts in room 1 at the west end. Whether either east room is obstructed is not stated in the initial condition, so the model designates four worlds and not one. A building nobody has surveyed is genuinely undetermined, and that is what makes the solution branch.
;; the sensing action: two events, one per answer, neither known in advance (:action inspect3 :parameters (?i - agent) :action-type (semi-private-sensing (e-inspect3-blocked ?i) (e-inspect3-clear ?i) ) :observability-conditions (:and (?i Fully) (default Partially) ) ) ;; knowing *whether*, not knowing *that* (:goal (and ([Kw. r1] (blocked-r3)) ([Kw. r1] (blocked-r6))))
Semi-private sensing says the agent that looks learns the answer, and anyone else present sees it look without learning what it saw. With one robot the distinction is invisible, and modelling it as fully public would still be a lie, one that stops being harmless the moment a second robot joins.
The policy
Aletheia picks its heuristic and strategy from the task's own features, and not from a flag, and reports which rule decided each:
[main] Heuristic: knowledge-spread (auto, rule 'kw-only-goal') [main] Strategy: AO* (auto, rule 'sensing-small-designated') [aostar] Solution found at depth 4 Expanded=32 Generated=35 Memo=6/6 [validator] OK: 4 leaves, 6 branches checked goto-door3_r1 ev0: inspect3_r1 ev0: goto-door6_r1 -> inspect6_r1 # room 3 seen blocked ev1: goto-door6_r1 -> inspect6_r1 # room 3 seen clear
Both branches continue to the second room, and they are distinct nodes, not a shared subtree. Which one runs is decided by an observation that has not been made when the plan is built: the definition of a policy as against a sequence.
The semantics
That the model designates four worlds and that the policy has four leaves are the same fact, and it is worth writing it out. Abbreviate the two undetermined propositions as \(B_3\) for blocked-r3 and \(B_6\) for blocked-r6. An epistemic state is a Kripke model \(\mathcal{M} = \langle W, \sim_{r_1}, V\rangle\) with a set \(W_d \subseteq W\) of designated worlds and[1, 2]
Nothing in the initial condition constrains either proposition and neither constrains the other, so the initial state is their product: \(W_0 = \{0,1\}^2\), four worlds, with \(\sim_{r_1} = W_0 \times W_0\) and every one of them designated. The goal is a conjunction of two knowing-whether formulas over the same agent,
and it is satisfied by four distinct states, one per assignment. Neither conjunct is entailed by anything in the initial model, and no ontic action in the domain affects either proposition: a wall does not move because a robot drove past it. The only events that change \(\sim_{r_1}\) are the two inspections.
inspect3 is an event model with one event per answer and no postconditions, whose preconditions partition the worlds:
In the product \(\mathcal{M}\otimes\mathcal{E}\) a world survives paired[3] only with the one event whose precondition it satisfies, and the acting agent's event relation is the identity, so no surviving pair is related to a pair carrying the other event. Four designated worlds therefore become two states of two worlds each, agreeing on \(B_3\) and still divided on \(B_6\). The second inspection does the same to \(B_6\), and each of the two states becomes two states of one world. Four leaves, and the depth is four because each inspection is preceded by the drive that makes it applicable.
The two conjuncts are independent, which is why the policy cannot share a subtree: the state in which room 3 was found blocked and the state in which it was found clear disagree about \(B_3\), and every formula evaluated below them is evaluated in a different model. They carry the same two action names and are distinct nodes.
Where the knowledge comes from
Nothing in the stack invents the answer. The perception node classifies a named region of the occupancy grid and reports what it found as the outcome of the sensing action the policy branched on:
epistemic_perception:
ros__parameters:
regions: ["room3", "room6"]
room3:
boxes: [4.25, 0.25, 11.8, 7.8]
atom: "blocked-r3"
atom_true_when_clear: false
sensing_action: "inspect3_r1"
outcome_when_clear: "e-inspect3-clear"
outcome_when_blocked: "e-inspect3-blocked"
A region is clear only when every cell in it has been observed and settled, blocked when any one cell is occupied, and undecided otherwise. Occupied beats unobserved, since no further looking removes an obstacle; unobserved beats free, since a region is clear only when all of it is.
The grid is built by slam_toolbox from the robot's own laser while it drives, and this is what makes the demonstration honest: a room the robot has not entered is unobserved in the grid and undetermined in the Kripke model at the same time. Those are two views of one fact. No prepared map is published anywhere in the system.
What building it found
Getting this to run end to end turned up five faults in the stack, each of which stopped the mission outright. All are fixed.
| Where | What was wrong |
|---|---|
| plansys2_executor | Rendering any policy killed the node with SIGSEGV: a range-for over get_parameter(...).as_string_array() iterated a destroyed vector and handed dlopen freed memory. Only bites when BT node plugins are configured, that is, only in the epistemic setup. |
| plansys2_bringup | regions: [] in the shipped params: an empty list has no element type, so perception threw at construction every time it was launched. |
| five packages | Rolling-only EventsExecutor and ServicesQoS made the fork unbuildable on the Humble its own CI targets. |
| plansys2_epistemic_perception | An observation arriving 78 ms before the executor's own update was refused as a model/world divergence and, by design, never retried, losing a reading the model was about to accept. |
| plansys2_epistemic_executor | With the observation applied first, the behaviour tree applied the same sensing action again and was refused, because its Kw precondition no longer held: it had succeeded. |
The demonstration also settled a modelling question the domain does not answer: what a robot should physically do when the policy says inspect3. A timed pause cannot tell success from failure. A rotating sweep only ever kept a stalled mapper alive. What the action does now is drive in, turn to face the room, hold still, and end exactly when (Kw r1 blocked-r3) holds, or fail and say so. A sensing action exists to acquire knowledge, so knowledge is what ends it.
One consequence is about sensors and not models. A region is blocked the instant one cell in it is occupied, but clear only when every cell has been observed and settled, which cannot be decided for a patch lying in open floor, because a 3.5 m laser returns nothing across a 7.5 m room and free space is traced only along beams that come back. The region a robot can settle is the one its beams cross on the way to a wall.
References