将不完美信息与超性质结合,揭示两种逻辑等价性
Strategy Logic, Imperfect Information, and Hyperproperties
- 用超性质视角重理解不完美信息的策略逻辑
- 证明两种逻辑在特定条件下可互相转换
- 适合形式化验证与多智能体系统研究者
策略逻辑(SL)是一种强大的时序逻辑,支持对多智能体系统(MAS)中策略行为的首等推理。在许多多智能体系统中,智能体及其策略无法观测系统全局状态,由此催生了多种围绕不完美信息的扩展,如带不完美信息的策略逻辑(SL$_\mathit{ii}$)。与此同时,研究者也探讨了策略行为与超性质的结合。超性质是关联系统多个执行路径的性质,常用于描述安全策略。超策略逻辑(HyperSL)是一种结合策略量化与执行路径间超性质表达能力的时序逻辑。本文研究 SL$_\mathit{ii}$ 与 HyperSL 之间的关系。主要结论是:在公式中无状态公式嵌套于路径公式的限制下,两者等价——可相互编码。前向编码基于不完美信息本身即为一种超性质的观察;后向编码则通过构建多智能体系统的自组合,利用不完美信息模拟超性质。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。