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

TL;DR

This paper introduces two new symbolic algorithms for model checking ATL* in multi-agent systems, demonstrating improved scalability and efficiency over existing methods through implementation and testing.

Contribution

It presents novel symbolic algorithms for ATL* model checking, including a parity-game reduction for infinite traces, with an implemented tool outperforming previous solutions.

Findings

Symbolic approach outperforms explicit-state methods

Parity-game algorithm is more scalable for infinite traces

Finite-trace verification is significantly faster

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*.