English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The decentralized perimeter surveillance system (DPSS) seeks to provide adecentralized protocol for evenly distributing surveillance of a perimeter overtime across an ensemble of unmanned aerial vehicles (UAVs) whose members maycommunicate only when in close proximity to each other. The protocol must alsoconverge to an even distribution of the perimeter in bounded time. Two versionsof the DPSS protocol presented in the original paper seem to converge inbounded time but only informal proofs and arguments are given. A laterapplication of model checking to these protocols found an error in one of thekey lemmas, invalidating the informal proof for one and casting doubt on theother. Therefore, a new hand proof of the convergence time for the simplerversion of the DPSS protocol or algorithm, Algorithm A or DPSS-A, was developedby Jeremy Avigad and Floris van Doorn. This paper describes a mechanization ofthat hand proof in the logic of ACL2 and discusses three specific ACL2utilities that proved useful for expressing and reasoning about the DPSS model.

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