Assuring Safety of Vision-Based Swarm Formation Control

TL;DR

This paper presents a formal safety assurance framework for vision-based swarm formation control, addressing perception errors and environmental variability through quantizer design and convergence analysis.

Contribution

It introduces a perception-consistent quantizer and adapts convergence analysis for vision-based formation control, enabling formal safety guarantees.

Findings

Quantizer in logarithmic polar coordinates is suitable for perception contracts.

Error bounds on vision perception are established using sampled data.

The formation control algorithm with the nonuniform quantizer converges reliably.

Abstract

Vision-based formation control systems are attractive because they can use inexpensive sensors and can work in GPS-denied environments. The safety assurance for such systems is challenging: the vision component's accuracy depends on the environment in complicated ways, these errors propagate through the system and lead to incorrect control actions, and there exists no formal specification for end-to-end reasoning. We address this problem and propose a technique for safety assurance of vision-based formation control: First, we propose a scheme for constructing quantizers that are consistent with vision-based perception. Next, we show how the convergence analysis of a standard quantized consensus algorithm can be adapted for the constructed quantizers. We use the recently defined notion of perception contracts to create error bounds on the actual vision-based perception pipeline using sampled data from different ground truth states, environments, and weather conditions. Specifically, we use a quantizer in logarithmic polar coordinates, and we show that this quantizer is suitable for the constructed perception contracts for the vision-based position estimation, where the error worsens with respect to the absolute distance between agents. We build our formation control algorithm with this nonuniform quantizer, and we prove its convergence employing an existing result for quantized consensus.