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

翻译：我们提出了两种新颖的符号算法，用于在无限迹和有限迹语义下对交替时序逻辑ATL*进行模型检测。特别地，针对无限迹，我们设计了一种新颖的符号化归约方法，将其转化为奇偶博弈问题。我们在ATL*AS模型检测器中实现了这两种方法，并使用合成基准测试集及一个网络安全场景对其进行了评估。我们的结果表明，符号化方法在性能上显著优于显式状态表示；同时我们发现，基于奇偶博弈的算法为无限迹验证提供了更具可扩展性和高效性的解决方案，其性能超越了现有工具。我们的结果也证实，有限迹模型检测相比无限迹验证能带来显著的性能优势。因此，我们为验证多智能体系统是否符合ATL*规约提供了一个全面的工具集。