Formal verification for multi-agent path execution in stochastic environments

Multi-agent pathfinding aims to determine conflict-free paths for multiple agents in a shared environment. However, real-world uncertainties can disrupt preplanned paths, leading to delays and new conflicts. Addressing these challenges requires robust strategies for path execution and adjustment. While many multi-agent pathfinding algorithms have been proposed, this work does not introduce a new algorithm. Instead, it presents an adjustment solution based on a set of constraint rules and a priority strategy to avoid conflicts and deadlocks. Additionally, a Markov decision process model is developed, derived from the preplanned paths, and integrated with the adjustment solution to account for stochastic environmental uncertainties. A novel integrated framework is proposed for formally analyze and verify the reliability of multi-agent path execution and the robustness of the adjustment solution in stochastic environments, with formal verification achieved through a logic-based probabilistic model checker. The performance of the proposed framework is validated through various scenarios on the Flatland platform. Results demonstrate that the adjustment solution, based on the constraint rules, effectively mitigates conflicts and deadlocks, improving robustness. Furthermore, formal verification proves effective in assessing the reliability and robustness of multi-agent path execution under uncertainty.