一句话：提出带策略量词的 HyperATL* 超逻辑，统一表达多智能体系统的策略性安全属性，并建立可判定且渐近最优的模型检测方法。
超属性用于描述系统中多条计算路径之间的关系，广泛服务于信息流安全等场景，但已有超逻辑难以刻画多智能体系统中的策略能力。本文提出 HyperATL*，在 CTL* 基础上引入路径变量与策略量词，使路径量化可由智能体联盟的策略选择来消解，从而统一表达多种（策略性）安全概念，并支持调度器选择影响执行速度的异步超属性。作者证明 HyperATL* 的有限状态模型检测可判定，给出基于交替自动机的算法，并证明其渐进最优匹配下界。作者还实现了一个针对该逻辑片段的原型模型检测器，可在小型有限状态系统中检查多种安全属性。
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.
@article{paperbot2214,
title = {HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems},
author = {Raven Beutner and Bernd Finkbeiner},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 2},
year = {2023},
doi = {10.46298/lmcs-19(2:13)2023}
}