德国亥姆霍兹信息安全中心（CISPA）最新论文《多智能体系统中的超属性逻辑》，42页pdf

摘要

超属性通常用于计算机安全中，以定义信息流策略和其他要求，这些要求对多个计算之间的关系进行推理。在本文中，我们研究了一类新的超属性，其中单个计算路径由多智能体系统中的智能体联盟策略来选择。我们介绍了 HyperATL*，这是计算树逻辑的扩展，带有路径变量和策略量词。我们的逻辑可以表达策略超属性，例如并发系统中的调度程序具有避免信息泄漏的策略。 HyperATL∗ 对于指定异步超属性特别有用，即在不同计算路径上的执行速度取决于调度程序选择的超属性。与其他最近用于规范异步超属性的逻辑不同，我们的逻辑是第一个允许对完整逻辑进行可判定模型检查的逻辑。我们提出了一种基于交替自动机的 HyperATL∗ 模型检查算法，并通过提供匹配的下界证明了我们的算法是渐近最优的。我们已经为 一部分HyperATL∗ 实现了一个原型模型检查器，能够检查小型程序的各种安全属性。