论文标题
HyperAtl*：多代理系统中超代理的逻辑
HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
论文作者
论文摘要
超构物是与系统中多个计算路径相关的系统属性，通常用于定义信息流策略。在本文中，我们研究了一类新型的超级专业，允许有关多代理系统中战略能力的推理。我们引入了HyperAtl*，这是使用路径变量和策略量词的计算树逻辑的扩展。我们的逻辑支持对系统中路径的定量 - 在诸如HyperCtl*之类的超时记中可能是可能的，但是根据代理联盟的战略选择来解决路径。这使我们能够在统一的超循环中捕获许多先前研究的（战略性）安全概念。此外，我们表明，HyperAtl*对于指定异步性超腐烂（即超专制）特别有用，在不同的计算路径上的执行速度取决于调度程序的选择。我们表明，HyperAtl*的有限状态模型检查是可以决定的，并基于交替的自动机提出了模型检查算法。我们确定我们的算法是通过证明匹配下限的渐近最佳选择。我们已经为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.
