Bidirectionality is Necessary in Cellular Machines for Exact-Arrival Multi-Agent Path Finding
Masashi Aono
cs.ET
Oct 19, 2026 · v1
cs.CC cs.DC cs.MA
TL;DR
Finite gadget lemmas and pair-invariance contradiction forms of the impossibility theorem are machine-checked in Lean 4 via Boolean encodings; other lemmas remain paper proofs.
Abstract
On ranked directed acyclic graphs coupled by vertex conflicts we study exact-arrival multi-agent path finding (departure and arrival pinned in place and time) posed as a distributed output task: every cell must emit its own bit of a valid joint path-support mask. The machines are cellular: one automaton per cell, state factored over cells, communication only along a fixed local fabric, synchronous rounds, a query-independent output round, no central decoder, and a per-topology transition code. "Necessary" here means: on an explicit hard topology, over all its feasible queries, no universally correct local-only architecture can renounce either temporal orientation; with global flags, impossibility becomes a bandwidth-round trade-off. The class is not vacuous: a flooding machine solves every instance in as many rounds as the diameter of the local fabric. The bound survives two concessions: we supply every agent's exact individual cavity, which alone solves the single-agent problem in zero rounds and makes the single-agent direction theorem vacuous; and we allow $k$ one-bit global aggregate flags. On a twelve-cell, two-agent, depth-three topology no forward-only machine with $k=0$ is correct on two feasible queries, for any number of rounds; the time-reversed topology does the same to backward-only machines. Placing $p$ copies side by side gives, for forward-only machines, $J_R+kR\ge p$ at constant depth, where $J_R$ measures how much of the query reaches the targets' cones and is $0$ here. A backward-only machine solves that family in constant rounds and a flag-streaming one in $\lceil p/k\rceil+O(1)$, so the bound is tight in order; on the composite family neither orientation can be renounced. The finite lemmas of the gadget and the pair-invariance contradictions are checked in Lean 4; the semantic bridge, the cone lemma and the counting are paper proofs. We report no benchmarks.
Problem
Exact-arrival multi-agent path finding on ranked DAGs with vertex conflicts is posed as a distributed output task for cellular machines. The question is whether such machines can renounce one temporal orientation of communication, forward-only or backward-only.
Approach
The authors define a class of cellular machines with factored per-cell state, local channels, and k one-bit global aggregate flags. Every agent's exact cavity is supplied as input. A twelve-cell, two-agent crossed-conflict gadget is built, along with side-by-side copies, to derive locality and counting lower bounds. The finite gadget lemmas and the pair-invariance contradictions are checked in Lean 4. The semantic bridge, the cone lemma and the counting arguments are paper proofs, cross-checked by Python enumeration.
Results
With k=0, no forward-only or backward-only machine is correct on the gadget's two feasible queries for any number of rounds. With flags, forward-only machines must satisfy J_R+kR≥p, and this bound is tight in order. On a composite family, neither orientation can be dropped.