资源介绍
在计算机科学和数理逻辑的交叉领域，交错时序逻辑（Alternating-Time Temporal Logics，简称ATL）是一类专门用于描述和分析多智能体系统中策略行为与时序性质的形式化工具。这类逻辑最初由阿卢尔、德拉姆和威廉姆斯在1997年前后提出，旨在解决并发系统中关于"群体是否能够通过协同策略来确保系统满足特定时序要求"这一核心问题。法国国家科学研究中心（CNRS）和巴黎-萨克雷大学ENS的斯蒂芬·德姆里教授在其最新著作中，以其在该领域数十年的深厚积累，为读者呈现了一部系统而精炼的学术导论。
这本书的核心目标，正如副标题所示，是帮助读者深入理解模型检测问题。所谓模型检测，就是如何自动判断一个给定的系统模型是否满足某个规范公式。对于ATL及其扩展逻辑ATL而言，这一问题涉及到策略的存在性验证、复杂度分析以及各种变体的可判定性探讨。德姆里在书中首先从并发博弈结构讲起，介绍了策略的基本概念和ATL的核心语法与语义，通过直观的机器人协作示例让抽象的逻辑公式变得易于理解。随后，作者逐步深入，探讨了ATL与分支时序逻辑（如CTL）之间的关系，以及不动点特征等理论内容。
本书的一大亮点在于其对复杂度问题的系统性处理。作者详细分析了从ATL到ATL*的模型检测复杂度演变，证明了MC(ATL*)的PSpace-硬度，并给出了在多项式空间中的求解方法。书中对偶游戏（parity games）的应用讲解尤为精彩，展示了如何将ATL*的模型检测问题转化为偶游戏问题，进而证明MC(ATL*)在2ExpTime中的完全性。此外，作者还专门讨论了位置策略在简化问题中的作用，以及不完全信息情况下的处理方法。
在书的后半部分，德姆里将注意力转向了一个前沿且富有挑战性的方向——资源感知逻辑。传统的ATL只关心策略能否实现目标，但在实际系统中，资源（如能量、内存）往往是受限的。作者引入了带资源的ATL变体（ATL*(x)），通过能量博弈的视角来建模资源约束下的策略推理，并深入探讨了这类逻辑的不可判定性和可判定子类的复杂性边界。这一部分内容对于研究嵌入式系统、机器人路径规划和网络安全等实际应用场景的读者具有重要参考价值。
作为计算机科学基础与应用逻辑丛书的一员，本书体现了该系列强调计算基础与数理逻辑互动的编辑理念。德姆里的写作风格严谨而不失可读性，全书配有丰富的练习题和详尽的参考文献导读，非常适合作为研究生教材或研究者入门读物。无论你是刚刚接触多智能体系统逻辑的初学者，还是希望系统梳理ATL理论体系的资深学者，这本书都能提供有价值的知识与洞见。它不仅是一本技术手册，更是一部记录了该领域发展脉络与研究前沿的学术指南。