We present CGAAL, our efficient on-the-fly model checker for alternating-time temporal logic (ATL) on concurrent game structures (CGS). We present how our tool encodes ATL as extended dependency graphs with negation edges and employs the distributed on-the-fly algorithm by Dalsgaard et al. Our tool offers multiple novel search strategies for the algorithm, including DHS which is inspired by PageRank and uses the in-degree of configurations as a heuristic, IHS which estimates instability of assignment values, and LPS which estimates the distance to a state satisfying the constituent property using linear programming. CGS are input using our modelling language LCGS, where composition and synchronisation are easily described. We prove the correctness of our encoding, and our experiments show that our tool CGAAL is often one to three orders of magnitude faster than the popular tool PRISM-games on case studies from PRISM's documentation and among case studies we have developed. In our evaluation, we also compare and evaluate our search strategies, and find that our custom search strategies are often significantly faster than the usual breadth-first and depth-first search strategies.

翻译：我们提出CGAAL——一种针对并发博弈结构(CGS)上交替时态逻辑(ATL)的高效即时模型检测工具。本文展示了如何将ATL编码为带否定边的扩展依赖图，并采用Dalsgaard等人提出的分布式即时算法。该工具为算法提供了多种新型搜索策略，包括受PageRank启发、以构型入度为启发信息的DHS，估计赋值值不稳定性的IHS，以及利用线性规划估计满足构成性质状态距离的LPS。CGS通过我们设计的建模语言LCGS输入，可便捷描述组合与同步过程。我们证明了编码的正确性，实验表明：在PRISM文档用例及我们开发的案例研究中，CGAAL比主流工具PRISM-games通常快1-3个数量级。评估中我们对比了各搜索策略，发现自定义搜索策略通常比常规广度优先和深度优先策略显著更高效。