Long-term Research Program
Epistemic robotics is the study of autonomous systems that maintain formal representations of knowledge, belief, and uncertainty, not only about the physical world, but about the epistemic states of other agents operating within it. This project develops planning formalisms, runtime architectures, and geometric reasoning tools grounded in Dynamic Epistemic Logic and the µ-calculus, targeting heterogeneous multi-robot fleets under partial observability and communication constraints.
The Problem
A robot navigating a warehouse, a drone team conducting search-and-rescue, a fleet of heterogeneous agents coordinating through communication blackouts, all share a challenge that classical task planning cannot address. The world is not fully observable, and the agents within it hold genuinely different, potentially inconsistent views of what is true.
Planning under partial observability requires more than probabilistic state estimation. It requires a robot to represent not only what it believes about the world, but what it believes other agents believe, and to plan actions that deliberately shape the epistemic state of the system as a whole. This is the problem of epistemic planning, and it demands a logic capable of reasoning about knowledge as a first-class object.
The following goals are not expressible in any classical planning formalism. They are epistemic goals, and they arise routinely in the deployment of autonomous multi-robot systems.
None of these goals have a representation in STRIPS, PDDL, or any classical planning formalism. They require an epistemic planner: a system whose state space is a structured model of what every agent knows, believes, and is uncertain about, in place of a set of ground atoms. The gap between classical planning and epistemic planning is a categorical difference in what kind of object constitutes a world state.
Formal Framework
The project is grounded in Dynamic Epistemic Logic (DEL)[1, 2], a modal framework for reasoning about how informational actions (sensing, announcement, communication) transform the knowledge states of agents. The central semantic object is the Kripke model: a labeled graph whose nodes are possible worlds and whose edges, indexed by agent, encode what each agent considers epistemically indistinguishable from its current vantage point.
The product update \(s \otimes a\) is the core operation. Given an epistemic state and an event model describing an action's physical and informational effects simultaneously, it computes the resulting epistemic state. Physical ontic effects, private sensing, and public communication are unified under this single operator.
Two structural properties bound the computational cost of runtime planning. An event model \(\mathcal{E}\) is self-absorbing if \(M \otimes \mathcal{E} \otimes \mathcal{E} \simeq M \otimes \mathcal{E}\) for all \(M\). Two event models \(\mathcal{E}, \mathcal{E}'\) are commutative if \(M \otimes \mathcal{E} \otimes \mathcal{E}' \simeq M \otimes \mathcal{E}' \otimes \mathcal{E}\) for all \(M\). When an event library satisfies these conditions, the Kripke model remains bounded in size under any sequence of updates, and the bisimulation contraction can be computed in linear time.
All agents simultaneously learn \(\varphi\). Accessibility relations collapse for \(\varphi\) across the group, establishing \(C_G\,\varphi\) in a single update.
The acting agent resolves its uncertainty about \(\varphi\). Others may observe that an action occurred without learning its outcome, a fundamental asymmetry in distributed systems.
Modifies the physical world via postconditions. Uninformed agents retain prior beliefs; the actor and any witnesses update via the product update accordingly.
Nested modalities \(\Box_i \Box_j \varphi\) encode what agent \(i\) believes agent \(j\) knows. Theory of Mind arises naturally from the Kripke semantics without additional machinery.
Integration
The modal µ-calculus and Dynamic Epistemic Logic occupy different levels of the same formal hierarchy. DEL specifies how Kripke models are transformed by informational actions; the µ-calculus specifies what must hold of those models via fixed-point formulas. When the models in question are epistemic states maintained and updated by the DEL product operation, the two formalisms compose into a unified framework for specifying and solving epistemic planning problems.
The µ-calculus extends propositional modal logic with a least fixed-point operator \(\mu X.\,\varphi(X)\) and a greatest fixed-point operator \(\nu X.\,\varphi(X)\), where \(X\) ranges over sets of worlds and \(\varphi\) is monotone in \(X\). By the Knaster–Tarski theorem, both operators are well-defined over the complete lattice \(2^W\). The standard modal operators \(\Box_i\) and \(\Diamond_i\) arise as degenerate fixed points: \(K_i\,\varphi = \Box_i\varphi\) and \(C_G\,\varphi = \nu X.\,\varphi \wedge \Box_G X\), so the epistemic language used in DEL is wholly contained within the modal µ-fragment.
The operative correspondence is between the two kinds of fixed-point computation that arise in epistemic planning. Reachability goals, where the robot must be able to reach a world satisfying \(\mathit{goal}\) through free worlds, are least fixed points of the operator \(\Phi(X) = \mathit{goal} \vee (\mathit{free} \wedge \Diamond X)\):
Safety and coherence properties, where the robot must remain within the region of known-free worlds for all future steps, are greatest fixed points:
Under epistemic uncertainty, unknown worlds are excluded from \(\mathit{free}\) in the least fixed-point computation. The planner treats unresolved space as unreachable until a sensing action contracts the epistemic state. This contraction is itself a form of greatest-fixed-point elimination: bisimulation contraction removes from \(W\) every world inconsistent with the observed outcome, exactly as \(\nu X.\,(\mathit{known} \wedge \Box X)\) removes worlds that fail the coherence condition. The two reductions, sensing-driven contraction in DEL and greatest-fixed-point elimination in the µ-calculus, operate on the same underlying lattice \(2^W\) and converge to the same canonical sub-model.
Define the epistemic transition system \(\mathcal{K}_{\mathrm{plan}}\) whose states are epistemic states and whose transitions are DEL product updates:
An epistemic planning task \((s_0, A, \varphi_g)\) asks whether there exists a sequence \(\pi = (a_1, \ldots, a_k)\) such that \(s_k \models \varphi_g\). This is equivalent to asking whether \(s_0\) belongs to the least fixed point of the reachability operator on \(\mathcal{K}_{\mathrm{plan}}\):
Epistemic planning is therefore µ-calculus model checking on \(\mathcal{K}_{\mathrm{plan}}\), where each node in the structure being checked is itself a Kripke model. When \(\varphi_g\) contains common knowledge (\(C_G\,\psi = \nu X.\,\psi \wedge \Box_G X\)), the goal formula is itself a \(\nu\)-formula, so the full planning problem involves a \(\mu\)-formula on \(\mathcal{K}_{\mathrm{plan}}\) whose leaves require evaluating a \(\nu\)-formula on object-level models \(M\). This two-level nesting of fixed-point operators is the formal structure that distinguishes epistemic planning from classical planning and from standard temporal verification: it is not, in general, reducible to either.
Occupancy Grid Semantics
The maps below ground µ-calculus fixed-point semantics in 2D occupancy grids, following the plan-extraction framework of Bárcenas et al. (2017): a plan is a tree of nodes satisfying a formula together with its subformulas in a Kripke structure, and the µ-calculus backward wavefront identifies precisely the set of worlds from which the goal is reachable. Each map exercises a qualitatively distinct planning scenario (multi-branch reachability, sensing-blocked propagation, dual-target branching, and νX safety) to illustrate why fixed-point logic, and not classical graph search, is the appropriate specification language[3, 4].
Three-phase animated plan extraction. Phase 1: the µ-calculus backward wavefront propagates from the goal, flooding all reachable free cells. Each shell \(X_k\) is the set of worlds from which the goal is reachable in at most \(k\) steps. Unknown cells block propagation until resolved. Phase 2: a private sensing event at the unknown corridor reveals free space; the wavefront resumes and crosses the previously blocked region. Phase 3: the certified path is extracted by greedy descent through the µX shells from the robot's initial position, tracing the unique shortest path to the goal through the saturated region.
Branching µX reachability with two disjoint targets. The wavefront propagates backward from both \(\mathit{goal}_1\) (top-right) and \(\mathit{goal}_2\) (bottom-right) simultaneously. Because the two goals lie on opposite sides of a central horizontal wall, no linear path satisfies both; the plan is an irreducibly branching tree rooted at \(w_0\), with one branch per target, a structure inexpressible in LTL but natural in the µ-calculus (Bárcenas et al. 2017, Theorem 6).
A narrow unknown corridor is the only passage to the goal. Before sensing, the least fixed-point halts: unknown cells are excluded from \(\mathit{free}\), so the wavefront cannot cross the corridor and the goal is unreachable under the current epistemic state. After a private sensing event \(E_{\mathrm{sense}}\) at the corridor entrance, the cells are revealed free, the product update contracts \(R_r\), and µX propagates through, establishing \(K_r(\mathit{free}(c))\) for each corridor cell and unlocking the plan.
Conjunction of two reachability formulas forces a two-branch plan. Agents \(R_1\) and \(R_2\) share a common prefix from the origin to the split junction, then diverge: \(R_1\) follows the µX branch to \(\mathit{goal}_A\) (upper corridor), \(R_2\) follows the µY branch to \(\mathit{goal}_B\) (lower corridor). Because the two goals are separated by an impassable wall, no single agent can satisfy both conjuncts in sequence; the conjunction itself demands the branching structure. Collision-freedom is guaranteed by the tree topology of the plan (Bárcenas et al. 2017, §2.2).
Greatest fixed-point contraction to the maximal safe sub-model. The iteration starts at \(S_0 = W\) and eliminates any cell failing \(\Box X\): cells with unknown neighbors are expelled because no guarantee holds for their successors. The surviving set is the maximal coherent known-free region; its boundary is the exploration frontier, the set of νX cells with at least one unknown neighbor. An epistemic planner selects frontier cells as sense targets, maximally expanding νX per step. This νX contraction and the DEL bisimulation contraction are two descriptions of the same canonical reduction on \(2^W\).
Formal Visualization
The following diagrams render the formal objects directly: worlds as labeled nodes, accessibility relations as directed edges, DEL events as explicit transformations, and µ-calculus fixed-point sets as color-coded membership.
Least fixed-point iteration on a Kripke navigation graph. Starting from \(X_0 = \emptyset\), each step propagates a wavefront backward from the goal world \(w_7\). At S₃, a private sensing event resolves \(w_3\) from unknown to free via a DEL product update, unblocking propagation through the upper branch. The blocked world \(w_4\) is permanently excluded from \(\mu X\).
Greatest fixed-point computation. Starting at \(S_0 = W\), worlds \(w_4\) and \(w_5\) are expelled: they are unknown with successors outside the known sub-graph. The surviving set \(\{w_0, w_1, w_2, w_3\}\) is the DEL bisimulation contraction of the epistemic state to its maximal coherent sub-model.
DEL product update \(s \otimes E_{\mathrm{sense}}\). After the update, only worlds where \(\mathrm{pre}(e) = p\) holds survive. Agent \(i\)'s relation \(R_i\) collapses: \(K_i\,p\) holds in \(s'\). Agent \(j\) retains its indistinguishability arc because it did not observe the sensing outcome.
Multi-Agent Coordination
The hardest problems arise when multiple robots must coordinate while operating in communication-restricted environments. Each robot maintains a local Kripke model of the system's joint epistemic state. When robots are connected, public announcements collapse accessibility relations and establish common knowledge. When they are disconnected, each robot evolves its model independently through DEL product updates over local observations alone.
Policies that actively disambiguate goal assignments minimize the epistemic term of the expected free energy. Robots signal intent through motion without explicit communication, resolving assignment conflicts that stalemate first-order reasoners.
Private sensing followed by public announcement. R₁ scouts the unknown gap via \(E_{\mathrm{sense}}\), contracting only \(R_{R_1}\) through the DEL product update and establishing \(K_{R_1}(\neg\mathit{blocked}(c_{\mathrm{gap}}))\). R₁ then broadcasts via \(E_{\mathrm{announce}}\), collapsing \(R_{R_2}\) as well and establishing \(C_G(\neg\mathit{blocked}(c_{\mathrm{gap}}))\) in a single further update. R₂, now informed, commits to the 15-step shortcut instead of the 21-step detour it would take under epistemic uncertainty.
Planning System
An epistemic planning task is a triple \((s_0, \mathrm{Act}, \varphi_g)\): an initial epistemic state, a finite set of epistemic actions, and a goal formula drawn from the full epistemic language. EPDDL operationalises this framework in a PDDL-compatible format through a structured library of action types, each corresponding to a distinct class of DEL event model. The four core types cover the full range of informational and physical effects that arise in multi-robot deployment.
All agents learn \(\varphi\) simultaneously. The accessibility relation collapses for \(\varphi\) across the group, establishing \(C_G\,\varphi\) in a single product update. Used to model broadcasts, shared sensor readings, and synchronisation points in multi-robot protocols.
The acting agent resolves its uncertainty about \(\varphi\); other agents observe that an action occurred but not its outcome. The product update contracts \(R_i\) while leaving \(R_j\) for \(j \neq i\) unchanged, the fundamental asymmetry modelled by the split product update in ALETHEIA.
Modifies the physical world via postconditions on atoms. Uninformed agents retain their prior beliefs about the changed proposition; the actor and any witnesses whose accessibility relations include the affected worlds update via the product update accordingly.
A subgroup \(G \subseteq \mathcal{A}\) learns \(\varphi\) while the remainder observes only that some announcement occurred. Intermediate between public and private: establishes \(C_G\,\varphi\) within the group without informing outsiders of the content, modelling whisper actions and side-channel communication.
Each action type maps to a distinct configuration of the event model \(\mathcal{E} = (E, Q, \mathrm{pre}, \mathrm{post}, E^*)\). The choice of \(|E^*|\) determines whether the planner produces a linear plan (ontic and public announcement actions, \(|E^*| = 1\)) or a conditional plan (sensing actions, \(|E^*| \geq 2\)), since each designated event corresponds to one branch of an AND-OR tree.
The ALETHEIA planner implements all four action types under a unified adaptive search framework. Three complementary aspects of its architecture directly reflect the structure of the action taxonomy above.
Sensing domains (|E*| ≥ 2) are routed to iterative-deepening AO* for conditional plan construction; deterministic domains use GBFS or EHC depending on state-space size and goal modal depth.
After every product update, the resulting Kripke model is reduced to its coarsest bisimilar quotient via partition refinement, preserving the truth of all modal formulae while keeping world counts tractable across iterated ontic and sensing sequences.
Four heuristics (\(h_{ug}\), \(h_{ed}\), \(h_{ks}\), \(h_{wc}\)) target distinct goal structures: unsatisfied conjunct count, epistemic distance in accessibility relations, knowledge-spread for Kw-goals, and designated world count for uncertainty reduction.
The goal language includes \(K_i\,\varphi\), \(\mathrm{Kw}_i\,\varphi\), and \(C_G\,\varphi\), each a fixed-point formula when unfolded, allowing goals of mixed epistemic depth to be satisfied simultaneously:
Four coordination domains built on these action types, together with the policies ALETHEIA returns for them and a 204-instance scaling study, are developed on a companion page: Coordination domains for UGV fleets. It executes the returned policies step by step, so the difference a single observability condition makes can be watched.
A policy is not a sequence, and half its preconditions are about what an agent knows. How that runs on ROS 2: the behaviour tree, its knowledge guards and DEL updates, and the epistemic state they consult.
A recorded run of the whole stack: an EPDDL mission whose goal is knowledge, a policy that branches on an observation not yet made, and the observation itself supplied by a map the robot builds with its own laser while it drives.
The RoboticsAcademy multi-robot Amazon warehouse exercise, on its own floor, with the uncertainty put back: the pallet is in one of two aisles, nobody knows which, and no sequence of actions delivers it. Solved for one robot, then two, then three.
Demonstrations
Every demonstration below is a recorded execution: an EPDDL domain grounded by plank, solved by Aletheia, executed by ePlanSys over ROS 2, and measured against a standalone epistemic state afterwards. They are grouped by the domain they run, and each group opens on request.
Six rooms and a measured floor. The routing is a µ-calculus fixed point over the occupancy grid, and the survey mission adds a goal stated as knowledge.
The six-room run Routing by a µ-calculus fixed point The six-room survey An EPDDL mission whose goal is knowledgeA pallet in one of two aisles, and a robot that may lift it only where it knows the pallet is. The same domain scales from one robot to three, deepens by one modal operator, and executes over an Open-RMF fleet.
The warehouse run One robot, then two, then three Nested epistemic goals What modal depth costs Over Open-RMF A floor RMF was never givenA leak in one of two suites on separate floors, under a goal with a secrecy conjunct. The domain admits private announcement and private ontic change, so the frame leaves S5 and two agents end the run holding beliefs the world contradicts.
The hotel incident Belief measured during a fleet missionReferences