Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a novel class of hyperproperties that allow reasoning about strategic abilities in multi-agent systems. We introduce HyperATL*, an extension of computation tree logic with path variables and strategy quantifiers. Our logic supports quantification over paths in a system - as is possible in hyperlogics such as HyperCTL* - but resolves the paths based on the strategic choices of a coalition of agents. This allows us to capture many previously studied (strategic) security notions in a unifying hyperlogic. Moreover, we show that HyperATL* is particularly useful for specifying asynchronous hyperproperties, i.e., hyperproperties where the execution speed on the different computation paths depends on the choices of a scheduler. We show that finite-state model checking of HyperATL* is decidable and present a model checking algorithm based on alternating automata. We establish that our algorithm is asymptotically optimal by proving matching lower bounds. We have implemented a prototype model checker for a fragment of HyperATL* that can check various security properties in small finite-state systems.

翻译：超性质是描述系统中多个计算路径之间关系的系统属性，常用于定义信息流策略等场景。本文研究一类新型超性质，其能够对多智能体系统中的策略能力进行推理。我们提出HyperATL*，一种扩展了计算树逻辑并引入路径变量与策略量词的形式系统。该逻辑支持对系统中的路径进行量化——正如HyperCTL*等超逻辑所实现的功能——但通过智能体联盟的策略选择来解析这些路径。这使得我们能够在一个统一的超逻辑框架中捕捉许多先前研究的（策略性）安全概念。此外，我们证明HyperATL*在描述异步超性质（即不同计算路径的执行速度由调度器的选择决定的超性质）方面尤为有效。我们证明了HyperATL*的有限状态模型检测问题可判定，并给出一种基于交替自动机的模型检测算法。通过证明匹配的下界，我们确认该算法在渐近意义下具有最优性。针对HyperATL*的一个片段，我们实现了原型模型检测器，能够在小型有限状态系统中验证多种安全属性。