CGAAL：带启发式的分布式即时 ATL 模型检测器
计算机科学中的逻辑
2023-10-03 v1
摘要
我们提出 CGAAL，一种用于并发博弈结构（CGS）上交替时序逻辑（ATL）的高效即时模型检测器。我们展示了我们的工具如何将 ATL 编码为带否定边的扩展依赖图，并采用 Dalsgaard 等人的分布式即时算法。我们的工具为该算法提供了多种新颖搜索策略，包括受 PageRank 启发并使用配置入度作为启发式的 DHS、估计赋值不稳定性的 IHS，以及使用线性规划估计到满足组成性质状态距离的 LPS。CGS 使用我们的建模语言 LCGS 输入，其中组合与同步易于描述。我们证明了编码的正确性，且实验表明我们的工具 CGAAL 在 PRISM 文档中的案例研究及我们开发的案例研究上，通常比流行工具 PRISM-games 快一到三个数量级。在我们的评估中，我们还比较并评价了搜索策略，发现自定义搜索策略通常显著快于常用的广度优先与深度优先搜索策略。
引用
@article{arxiv.2310.00999,
title = {CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics},
author = {Falke B. Ø. Carlsen and Lars Bo P. Frydenskov and Nicolaj Ø. Jensen and Jener Rasmussen and Mathias M. Sørensen and Asger G. Weirsøe and Mathias C. Jensen and Kim G. Larsen},
journal= {arXiv preprint arXiv:2310.00999},
year = {2023}
}
备注
In Proceedings GandALF 2023, arXiv:2309.17318