The formal verification of multi-agent systems in safety-critical domains is challenged by the need to certify population-level behaviours, such as formation control, under environmental uncertainty. Traditional state-based verification techniques are often inadequate for expressing these system-wide objectives and face scalability limitations. This thesis addresses this gap by developing a distributional reachability framework that models the evolution of the system directly over the space of probability distributions, using Interval Markov Decision Processes (IMDPs) to capture model uncertainty. We introduce two complementary analysis algorithms to compute guaranteed bounds on the set of all reachable distributions: a forward method using occupation measures and McCormick relaxations, and a robust backward algorithm based on value iteration over a discretised distribution space. Case studies in swarm deployment demonstrate the efficacy of the framework in computing robust, set-based approximations of reachable distributions. Furthermore, results for the robust backward reachability algorithm are presented for a running example. This capability allows for the formal verification of complex distributional specifications and the synthesis of control policies with certified safety guarantees, establishing a computational foundation for designing certifiably safe, large-scale autonomous systems.

Trajectory prediction is a key element of autonomous vehicle systems, enabling them to anticipate and react to the movements of other road users. Robustness testing through adversarial methods is essential for evaluating the reliability of these prediction models. However, current approaches tend to focus solely on manipulating model inputs, which can generate unrealistic scenarios and overlook critical vulnerabilities. This limitation may result in incomplete assessments of model performance in real-world conditions. The specific effects of more comprehensive adversarial attacks on trajectory prediction models have not been thoroughly investigated. In this work, we demonstrate that by perturbing both model inputs and anticipated future states, we can uncover previously undetected weaknesses and provide a more realistic evaluation of model robustness. Our novel approach incorporates dynamical constraints and preserves tactical behaviors, enabling more effective and realistic adversarial attacks. We introduce new performance measures to assess the realism and impact of these adversarial trajectories. Testing our method on a state-of-the-art prediction model reveals significant increases in prediction errors and collision rates under adversarial conditions. Qualitative analysis further shows that our attacks can expose critical weaknesses, such as the model’s inability to detect potential collisions in what appear to be safe predictions. These results underscore the need for more comprehensive adversarial testing to better evaluate and improve the reliability of trajectory prediction models for autonomous vehicles. To support further research in this area, we provide an open-source framework for studying adversarial robustness in trajectory prediction. This work advances adversarial testing techniques, contributing to the safety and reliability of autonomous driving systems.