A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A

TL;DR

This paper presents a formal, mechanized proof in ACL2 confirming that the simplified DPSS Algorithm A guarantees bounded convergence time for decentralized perimeter surveillance using UAVs.

Contribution

It provides the first formal, mechanized proof of the bounded convergence time for the DPSS Algorithm A, improving upon previous informal proofs and addressing earlier errors.

Findings

Mechanized ACL2 proof confirms bounded convergence time.

Identifies useful ACL2 utilities for modeling distributed algorithms.

Addresses and corrects previous proof errors.

Abstract

The decentralized perimeter surveillance system (DPSS) seeks to provide a decentralized protocol for evenly distributing surveillance of a perimeter over time across an ensemble of unmanned aerial vehicles (UAVs) whose members may communicate only when in close proximity to each other. The protocol must also converge to an even distribution of the perimeter in bounded time. Two versions of the DPSS protocol presented in the original paper seem to converge in bounded time but only informal proofs and arguments are given. A later application of model checking to these protocols found an error in one of the key lemmas, invalidating the informal proof for one and casting doubt on the other. Therefore, a new hand proof of the convergence time for the simpler version of the DPSS protocol or algorithm, Algorithm A or DPSS-A, was developed by Jeremy Avigad and Floris van Doorn. This paper describes a mechanization of that hand proof in the logic of ACL2 and discusses three specific ACL2 utilities that proved useful for expressing and reasoning about the DPSS model.