New Spatio-Temporal Logic Extension Monitors Multi-Agent Communication Diameters

Verification of multi-agent systems that move through continuous space and time requires logic expressive enough to capture entangled spatio-temporal properties. Existing muTGL logic handles many such properties but lacks the ability to analyze reachability within specific distance bounds or track the length of communication chains—critical for decentralized monitoring and graph-theoretic analysis of distributed protocols.

To address this, Lydia Bakiri, Jérémy Dubut, and Sergio Mover introduce an extension of muTGL with a new operator called the space horizon. This operator bounds the distance of communication chains, enhancing expressiveness to encode reachability and escaping modalities previously unavailable. They provide a centralized offline monitoring algorithm and validate it on simulations of Consensus-Based Bundle Algorithms (CBBA) for task allocation. This work bridges the gap between spatio-temporal logic and practical distributed system verification.