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*的一个子片段，我们实现了原型模型检测器，能够对小型有限状态系统的各类安全属性进行验证。