Safe and stabilizing distributed multi-path cellular flows

We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (robots, vehicles, etc.) within each geographic partition (cell) is the same. Each cell is controlled by software to move entities across the cell to route entities from sources to targets without collisions. We present a formal model of a distributed traffic control protocol that guarantees minimum separation between entities, even as the software controlling some cells fails by crashing. The distributed traffic control protocol relies on two principles: (a) temporary blocking entity transfers between adjacent cells for maintenance of safety and (b) local geographical routing for guaranteeing progress of entities to their targets. Establishing liveness in distributed traffic control systems is challenging, but liveness analysis will be necessary to apply distributed algorithms in applications like coordinating robot swarms and intelligent highway systems. Once new failures stop occurring, in the case of a single target cell, the protocol is guaranteed to self-stabilize and entities with feasible paths to the target cell make progress towards it. For multiple targets, failures may cause deadlocks in the system, so we identify a class of non-deadlocking failures where all entities are guaranteed to make progress to their respective targets. Our assertional proofs may serve as templates for the analysis of other distributed traffic control protocols. We also present simulation results to validate the formal model, and to provide estimates of entity throughput as a function of entity velocity, safety separation distance, single-target path complexity, failure-recovery rates, and multi-target path complexity.