The Epistemic Robotics Project

The four cases

Two axes: how many agents, and knowledge or belief

Adding an agent indexes the modality. Dropping the truth axiom turns knowledge into belief. The four pages below treat the four combinations, each through a domain that reaches it. All domains places every domain of the repository in one of them.

The planning task

Epistemic states, event models, and conditional policies

An epistemic state is a multi-pointed Kripke model \(\mathcal{M} = (W, \{R_i\}_{i\in\mathcal{A}}, V, W^{*})\): the worlds a fleet considers possible, one indistinguishability relation per vehicle, a valuation, and the designated set \(W^{*}\) of candidates for the actual world. Knowledge is \(\mathrm{S5}\), so each \(R_i\) is an equivalence.

An action is an event model \(\mathcal{E} = (E, \{Q_i\}, \mathrm{pre}, \mathrm{post}, E^{*})\), applied by product update. The relation \(Q_i\) carries the entire modelling commitment: a vehicle that relates every event to a distinguished null event is oblivious, it observes neither the outcome of the action nor its occurrence.

A sensing action has \(|E^{*}| \ge 2\), one designated event per reading, so a solution takes the form of a policy: an AND/OR tree whose OR-nodes choose an action, whose AND-nodes branch over designated events, and every leaf of which satisfies the goal. Goals here are modal:

The third is the one no non-epistemic encoding expresses: it requires one vehicle to be informed and another to remain ignorant, so no scalar measure of "how much the fleet knows" can serve as a goal test.

The four domains

One facility, four observability models

All four domains share a corridor of \(L\) bays, a fleet of \(N\) UGVs, a target confined to \(U\) candidate bays, movement as a public ontic action, and sensing as strictly private: a vehicle reads only the bay it occupies, and no teammate observes the reading. What differs is the communication action.

Observability as a formula

Range limitation is not a special case in the planner; it is an observability condition evaluated per agent at update time. This is the single block in which ugv-radio differs from ugv-public:

(:action report
    :parameters (?i - agent ?l - location)
    :action-type (private-announcement (e-report ?i ?l) (nil))
    :observability-conditions
        (:and
            (?i Fully)
            (:forall (?j - agent | (/= ?i ?j))
                (?j
                    (if
                        (forall (?l1 - location)
                            (imply (at ?i ?l1)
                                (exists (?l2 - location |
                                        (or (= ?l2 ?l1) (adjacent ?l1 ?l2) (adjacent ?l2 ?l1)))
                                    (at ?j ?l2) )))
                        Fully
                    else
                        Oblivious ) ) )
            (default Oblivious) )
)

Capability interlock

When an ontic action is the precondition of an epistemic one

In ugv-facility the fleet is heterogeneous: \(R_2\) carries the key but no detector, \(R_1\) the reverse, and a mid-corridor bay starts locked. Neither vehicle can complete the mission alone, and the dependency runs across the ontic/epistemic boundary, \(R_2\) must change the world before \(R_1\) can learn anything at all.

Measurements

What drives the cost plank

204 instances, grounded with plank and solved with ALETHEIA under a 60 s search budget. The suite varies fleet size \(N\), corridor length \(L\), initial uncertainty \(U\), which is exactly \(|W|\), deployment, goal shape, and the number of items.

Medians over solved instances. All eight unsolved instances are range-limited with four candidate bays and three or more vehicles; every one is a search timeout and not an error. Grounding, by contrast, scales with \(N \times L\): from 0.02 s to 76 s across the same suite, an offline, cacheable cost, where search is the online one.

The catalogue

Domains in this repository, and the frames they reach

The domains below are stated in EPDDL over the intermediate action-type library, which supplies ontic change, sensing and announcement in public, semi-private, quasi-private and private forms. The observability conditions an action declares determine which frame the reachable state space has, so the frame is a consequence of the vocabulary a domain uses.

They are grouped by the logic their reachable models inhabit. Each tier extends the one above it: the language gains an index, then the frame gives up an axiom. The axiom schemas and the frame conditions they correspond to are stated with each tier, since the correspondence is what makes the frame a property that can be measured off a run.

Belief

Where \(\mathrm{S5}_n\) stops being enough

An \(\mathrm{S5}_n\) model has an accessibility relation that is an equivalence, and reflexivity is the clause that makes knowledge factive: \(K_i\varphi \rightarrow \varphi\). An agent in such a model can be ignorant to any degree and its beliefs remain true. Every domain in the upper half of the table stays inside that fragment, because every action they declare is observed by all agents or by none in a way that leaves each agent's equivalence class containing the world that holds.

Two constructions leave it. A private-ontic action changes the world while some agents observe nothing, so an agent that formed a true belief before the change carries it afterwards, when it is false. A private-announcement informs part of the group, and the agents outside the audience continue in a world the message has already excluded. In both cases the agent's relation loses the self-loop at the actual world, the frame becomes \(\mathrm{KD45}_n\), and \(K_i\) is read as belief.

This is a property of the run and it can be measured. The hotel incident reports the accessibility relation of every agent after every action of an executed mission. Two agents lose reflexivity, at two identifiable steps, under the two constructions above:

The model also grows at those two steps, from two worlds to four and then to five. A private action introduces the distinction between the world in which it occurred and the world its non-observers continue to occupy, and the model has to carry both.

doxastic-depot is the domain written to exercise this deliberately. Every relocation in it is private, so a crate moved once leaves every agent outside the source bay believing it is where it was; its five instances plant a false belief, plant a second-order false belief, repair one into common knowledge, and turn private knowledge into common knowledge by announcement.

The stack

From a domain to a fleet

A domain in this repository is a source file, and reaching a robot from there involves four components with distinct responsibilities.

plank parses the domain, its instance and the action-type library, checks their types, and grounds the lifted actions into the tokens a planner searches over. It also validates a plan independently, which is how a policy is checked against something other than the planner that produced it.

Aletheia searches over pointed Kripke models. Its unit of progress is the product update, so a sensing action with several outcomes produces several successors and the result is a policy with a branch at that action. The nested-goal study measures what the shape of the goal costs this search.

eplansys executes the policy on ROS 2. Its executor renders the policy as a behaviour tree, one node per policy node, each guarded by the knowledge its action requires and followed by the update its outcome determines. Its epistemic state holds the model and applies that update. The state answers two questions any component may ask: check_formula evaluates a modal formula, and get_agent_perspective returns the model as one agent sees it. The measured figures in the run reports are built from those two services.

The performer is whatever drives the hardware. For a fleet it is eplansys_rmf_bridge, which submits one Open-RMF task per action, pins it to the robot the planner named, and reports what the robot observed. Open-RMF decides lifts, doors, floor space and traffic between fleets, and holds no representation of knowledge; the Kripke model holds no representation of a lift. Each system decides what it can represent.

The return path

A sensing action's outcome selects the branch, so the outcome has to travel from the performer back to the state. plansys2_msgs/ActionExecution carries an outcome field for it, and the value is the name of an event the action's model declares. A performer that reports an event the policy does not list fails its branch, which is the treatment any unanticipated observation receives. An ordinary action leaves the field empty, and every classical performer does so.

Open issue

A benchmark that discriminates

... broadcast_R1_o2_b2 -> unlock_R2_b2_b3
    -> move_R1_b2_b3 -> move_R1_b3_b4 -> scan_R1_o1_b4   [leaf]

Three checks locate the fault in the planner and not the encoding. plank's independent validator reports the goal unsatisfied on the same history; the identical model with a goal naming only the last-sensed atom is solved correctly, with the broadcast present; and all 190 corridor and addressed-radio policies end in a communication action, as does every single-item facility policy. Only goals conjoining knowledge requirements over two distinct atoms exhibit it.

Goal shape, knowing-whether, nested, negated, conjoined over several atoms, deserves standing as a benchmark dimension alongside instance size. Scaling a suite exercises one code path harder; varying the shape of the goal exercises different ones.

A planner's own plan validator cannot adjudicate this class of disagreement, since it shares the state pipeline under suspicion. The cross-check that settled it came from a second, independent implementation of the semantics.