Distributed Continuous Aerial Surveillance by UAS Swarms Under Formal Mission Specifications
Persistent aerial surveillance using multi-unmanned aerial systems (UASs) requires decentralized coordination, continuous team reconfiguration, and provable mission correctness despite limited onboard energy and communication constraints. This paper develops a distributed framework for continuous aerial surveillance under bounded Linear Temporal Logic (LTL) mission specifications. The proposed approach partitions the UAS team into stationary anchors and mobile workers operating under cyclic replacement modes, and constructs a deep neural network (DNN)-inspired communication topology that enables fully decentralized coordination through local interactions. A hierarchical bounded LTL specification formally captures mode-to-mode reference consistency, cyclic team rotation, finite-time reachability, trajectory tracking, and prescribed surveillance coverage. By proving the finite-time convergence of the worker-agent coordination dynamics, the paper guarantees the finite-time satisfaction of the mission specification. To maximize sensing effectiveness, an information-theoretic optimization framework synthesizes the reference configuration of newly deployed worker agents by minimizing the Kullback--Leibler divergence between the surveillance-node distribution and the induced coverage density. The resulting reference configuration uniquely determines a deterministic, mode-dependent communication topology, eliminating online communication-graph optimization while preserving the formal mission guarantees. Finally, a decentralized quadrotor controller realizes the distributed references using only local communication. Numerical simulations demonstrate cyclic team reconfiguration, decentralized communication-topology synthesis, finite-time formation convergence, and certified persistent surveillance coverage.