Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems
Yan Kim, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci
TL;DR
The paper tackles the challenge of scalable verification for real-time multi-agent systems by extending variable-based abstraction to timed, modular MAS models. It introduces Timed Agent Graphs (TAG) and Timed MAS Graphs (TMAS) to encode clocks, discrete variables, and synchronized interactions, and proves correctness of the abstraction for the universal fragment of $TCTL$, along with theoretical complexity considerations. A key contribution is a lossy, variable-based abstraction that operates on modular specifications without generating explicit global state spaces, enabling practical verification. The work demonstrates the approach with an experimental evaluation on a simplified Estonian voting scenario using the Uppaal model checker, highlighting its potential for real-time MAS verification in industrial-scale settings.
Abstract
Model checking of temporal logics in a well established technique to verify and validate properties of multi-agent systems (MAS). However, practical model checking requires input models of manageable size. In this paper, we extend the model reduction method by variable-based abstraction, proposed recently by Jamroga and Kim, to the verification of real-time systems and properties. To this end, we define a real-time extension of MAS graphs, extend the abstraction procedure, and prove its correctness for the universal fragment of Timed Computation Tree Logic (TCTL). Besides estimating the theoretical complexity gains, we present an experimental evaluation for a simplified model of the Estonian voting system and verification using the Uppaal model checker.