Formal Verification of Probabilistic Multi-Agent Systems for Ballistic Rocket Flight Using Probabilistic Alternating-Time Temporal Logic
Damian Kurpiewski, Jędrzej Michalczyk, Wojciech Jamroga, Jerzy Julian Michalski, Teofil Sidoruk
TL;DR
The paper tackles safety verification for ballistic rocket flight modeled as probabilistic multi-agent systems. It develops a PATL-based framework to reason about strategic capabilities under uncertainty, combining real telemetry with high-fidelity simulation. By comparing non-probabilistic and probabilistic models under imperfect information, it demonstrates trade-offs between fidelity and tractability and provides guidance on confidence thresholds for critical safety properties. The Perun case study showcases practical applicability to commercial spaceflight and highlights avenues for reducing state-space complexity and advancing verification under uncertainty.
Abstract
This technical report presents a comprehensive formal verification approach for probabilistic agent systems modeling ballistic rocket flight trajectories using Probabilistic Alternating-Time Temporal Logic (PATL). We describe an innovative verification framework specifically designed for analyzing critical safety properties of ballistic rockets engineered to achieve microgravity conditions for scientific experimentation. Our model integrates authentic flight telemetry data encompassing velocity vectors, pitch angles, attitude parameters, and GPS coordinates to construct probabilistic state transition systems that rigorously account for environmental stochasticity, particularly meteorological variability. We formalize mission-critical safety properties through PATL specifications to systematically identify trajectory deviation states where the rocket risks landing in prohibited or hazardous zones. The verification framework facilitates real-time safety monitoring and enables automated intervention mechanisms, including emergency engine disengagement protocols, when predefined safety thresholds are exceeded. Experimental validation demonstrates the practical effectiveness and reliability of our approach in ensuring mission safety while maintaining scientific mission objectives.