Strategy logic (SL) is a powerful temporal logic that enables first-class reasoning over strategic behavior in multi-agent systems (MAS). In many MASs, the agents (and their strategies) cannot observe the global state of the system, leading to many extensions of SL centered around imperfect information, such as strategy logic with imperfect information (SL$_\mathit{ii}$). Along orthogonal lines, researchers have studied the combination of strategic behavior and hyperproperties. Hyperproperties are system properties that relate multiple executions in a system and commonly arise when specifying security policies. Hyper Strategy Logic (HyperSL) is a temporal logic that combines quantification over strategies with the ability to express hyperproperties on the executions of different strategy profiles. In this paper, we study the relation between SL$_\mathit{ii}$ and HyperSL. Our main result is that both logics (restricted to formulas where no state formulas are nested within path formulas) are equivalent in the sense that we can encode SL$_\mathit{ii}$ instances into HyperSL instances and vice versa. For the former direction, we build on the well-known observation that imperfect information is a hyperproperty. For the latter direction, we construct a self-composition of MASs and show how we can simulate hyperproperties using imperfect information.
翻译:策略逻辑(SL)是一种强大的时序逻辑,能够对多智能体系统(MAS)中的策略行为进行一阶推理。在许多多智能体系统中,智能体(及其策略)无法观测系统的全局状态,这催生了以不完全信息为核心的多类策略逻辑扩展,例如不完全信息策略逻辑(SL$_\mathit{ii}$)。在另一研究方向上,学者们探索了策略行为与超性质的结合。超性质是关联系统多个执行轨迹的系统性质,在安全策略规约中尤为常见。超策略逻辑(HyperSL)是一种时序逻辑,它融合了策略量词与对不同策略剖面执行轨迹的超性质表达能力。本文研究了SL$_\mathit{ii}$与HyperSL之间的关联。我们的核心结论是:在限定状态公式不嵌套于路径公式的前提下,两种逻辑具有等价性,即SL$_\mathit{ii}$实例可编码为HyperSL实例,反之亦然。对于前向编码,我们基于“不完全信息即超性质”这一经典观察进行构建;对于逆向编码,我们通过构造多智能体系统的自组合,展示了如何利用不完全信息模拟超性质。