@article{johnson2015tcs,
    author      =   {Taylor T. Johnson and Sayan Mitra},
    title       =   {Safe and Stabilizing Distributed Multi-Path Cellular Flows},
    year        =   {2015},
    journal     =   {Theoretical Computer Science},
    publisher   =   {Elsevier},
    address     =   {},
    volume      =   {},
    number      =   {},
    issn        =   {},
    doi     =   {10.1016/j.tcs.2015.01.023},
    pages       =   {1--46},
    month       =   feb,
    pdf = {http://www.taylortjohnson.com/research/johnson2015tcs.pdf},
    software = {https://bitbucket.org/verivital/cell_flows},
    abstract    =   {We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (vehicles) within each partition (cell) is coupled.  Establishing liveness in such systems is challenging, but such analysis will be necessary to apply such distributed traffic control algorithms in applications like the intelligent highway system and for coordinating robot swarms.  We present a distributed traffic control protocol that guarantees minimum separation between vehicles, even as some cells fail.  Once new failures cease occurring, in the case of a single target, the protocol is guaranteed to self-stabilize and the vehicles 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 vehicles are able to make progress to their respective targets.  The algorithm relies on two general principles: temporary blocking for maintenance of safety and local geographical routing for guaranteeing progress.  Our assertional proofs may serve as a template for the analysis of other distributed traffic control protocols.  We present simulation results that provide estimates of throughput as a function of vehicle velocity, safety separation, single-target path complexity, failure-recovery rates, and multi-target path complexity.},
}