Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) quantification over strategies and provides a logical framework to express many important properties such as Nash equilibria, dominant strategies, etc. While in SL the same strategy can be used in multiple strategy profiles, each such profile is evaluated w.r.t. a path-property, i.e., a property that considers the single path resulting from a particular strategic interaction. In this paper, we present Hyper Strategy Logic (HyperSL), a strategy logic where the outcome of multiple strategy profiles can be compared w.r.t. a hyperproperty, i.e., a property that relates multiple paths. We show that HyperSL can capture important properties that cannot be expressed in SL, including non-interference, quantitative Nash equilibria, optimal adversarial planning, and reasoning under imperfect information. On the algorithmic side, we identify an expressive fragment of HyperSL with decidable model checking and present a model-checking algorithm. We contribute a prototype implementation of our algorithm and report on encouraging experimental results.

翻译：策略逻辑（SL）是一种强大的时序逻辑，能够在多智能体系统中进行策略推理。SL支持对策略的显式（一阶）量化，并提供逻辑框架以表达纳什均衡、占优策略等许多重要性质。尽管在SL中同一策略可被用于多个策略组合，但每个策略组合均依据路径性质（即考虑特定策略交互产生的单一路径的性质）进行评估。本文提出超策略逻辑（HyperSL），这是一种能够比较多个策略组合结果的策略逻辑，其比较依据为超性质（即关联多条路径的性质）。我们证明HyperSL可捕获SL无法表达的若干重要性质，包括非干扰性、量化纳什均衡、最优对抗规划及不完全信息下的推理。在算法层面，我们识别出HyperSL中具有可判定模型检测能力的一个表达力丰富的片段，并给出对应的模型检测算法。我们贡献了该算法的原型实现，并报告了令人鼓舞的实验结果。