ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems

TL;DR

The paper tackles scalable verification of strategic abilities in multi-agent systems by developing symbolic model-checking methods for both finite-trace ATL$_f^*$ and infinite-trace ATL$^*$, implemented in the ATL$^*$AS tool. It introduces a symbolic product and fixpoint approach for ATL$_f^*$ over finite traces and a symbolic parity-game reduction for ATL$^*$ over infinite traces, backed by a full toolchain with multiple backends and automata translations. Empirical results on synthetic benchmarks and a cybersecurity scenario show that symbolic finite-trace verification dramatically outperforms explicit-state methods, and parity-game-based infinite-trace verification scales favorably compared to prior approaches and to MCMAS-SL[1G]. Finite-trace verification is consistently more tractable than infinite-trace verification, highlighting practical guidance for modeling MAS when finite executions suffice. The work provides a scalable, publicly available tool for verifying ATL$^*$ specifications in real-world multi-agent contexts, with significant implications for secure system design and automated reasoning about strategic behavior.

Abstract

We present two novel symbolic algorithms for model checking the Alternating-time Temporal Logic ATL*, over both the infinite-trace and the finite-trace semantics. In particular, for infinite traces we design a novel symbolic reduction to parity games. We implement both methods in the ATL*AS model checker and evaluate it using synthetic benchmarks as well as a cybersecurity scenario. Our results demonstrate that the symbolic approach significantly outperforms the explicit-state representation and we find that our parity-game-based algorithm offers a more scalable and efficient solution for infinite-trace verification, outperforming previously available tools. Our results also confirm that finite-trace model checking yields substantial performance benefits over infinite-trace verification. As such, we provide a comprehensive toolset for verifying multiagent systems against specifications in ATL*.

Figures (9)

• Figure 1: Overview of ATL$^*$AS tool architecture, showing the modular design of the frontend, automata generation pipeline, and solver backends. Dashed rectangles indicate the external components used.
• Figure 2: Exp. 1 -- Comparison of runtime performance between the explicit and symbolic model checkers.
• Figure 3: Exp. 2 -- Runtime of the explicit and symbolic model checkers as formula size increases. Marker colour indicates the tool used for DFA generation. Dashed lines show fitted linear and exponential curves.
• Figure 4: Exp. 1: Comparison of runtime versus model size for finite-trace (explicit and symbolic) and infinite-trace (parity-game–based) model checkers.
• Figure 5: Exp. 2: Comparison of runtime versus formula size for finite-trace (explicit and symbolic) and infinite-trace (parity-game–based) model checkers.

Theorems & Definitions (10)

• Definition 2.1: CGS
• Definition 2.2: Model Checking Problem
• Definition 2.3: DFA
• Definition 2.4: DPA
• Definition 2.5: Parity Game
• Definition 3.1: Product of CGS and DFA
• Definition 3.2: Safety Set and Safety Game
• Theorem 3.1: Soundness of Alg. \ref{['alg:game-solving-finite']}
• Definition 4.1: Parity Game from CGS and DPA
• Theorem 4.1: Soundness of Alg. \ref{['alg:parity-infinite']}