Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strategy Logic, Imperfect Information, and Hyperproperties

Raven Beutner, Bernd Finkbeiner

TL;DR

This work establishes a formal equivalence between two rich logics for multi-agent strategic reasoning: Strategy Logic with Imperfect Information ($SL_{\u204e{\it ii}}$) and Hyper Strategy Logic (HyperSL), restricted to fragments with no nested state formulas inside path formulas. It provides mutually constructive encodings: (i) encoding $SL_{\u204e{\it ii}}$ into HyperSL by treating imperfect information as a hyperproperty, and (ii) encoding HyperSL into $SL_{\u204e{\it ii}}$ via self-composition of the underlying multi-agent system to simulate multiple executions under imperfect information. The encodings come with explicit constructions and size bounds, leveraging injective labeling and action recording to enforce information constraints and a self-composition technique to model hyperproperties as ordinary path-based properties. The results offer a unified perspective on knowledge and hyperproperties in MASs and open avenues for transferring decidability insights and verification strategies between the two frameworks, albeit noting undecidability for model checking in general. Overall, the paper advances the theoretical understanding of how imperfect information and hyperproperties relate in strategic settings and suggests practical directions for leveraging existing verification tools across these formalisms.

Abstract

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.

Strategy Logic, Imperfect Information, and Hyperproperties

TL;DR

This work establishes a formal equivalence between two rich logics for multi-agent strategic reasoning: Strategy Logic with Imperfect Information () and Hyper Strategy Logic (HyperSL), restricted to fragments with no nested state formulas inside path formulas. It provides mutually constructive encodings: (i) encoding into HyperSL by treating imperfect information as a hyperproperty, and (ii) encoding HyperSL into via self-composition of the underlying multi-agent system to simulate multiple executions under imperfect information. The encodings come with explicit constructions and size bounds, leveraging injective labeling and action recording to enforce information constraints and a self-composition technique to model hyperproperties as ordinary path-based properties. The results offer a unified perspective on knowledge and hyperproperties in MASs and open avenues for transferring decidability insights and verification strategies between the two frameworks, albeit noting undecidability for model checking in general. Overall, the paper advances the theoretical understanding of how imperfect information and hyperproperties relate in strategic settings and suggests practical directions for leveraging existing verification tools across these formalisms.

Abstract

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). 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 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 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.

Paper Structure

This paper contains 26 sections, 6 theorems, 28 equations.

Table of Contents

  1. Introduction
  2. Strategy Logic With Imperfect Information
  3. Hyper Strategy Logic
  4. The Connection
  5. Preliminaries
  6. Concurrent Game Structures
  7. SL$_{\mathit{ii}}$
  8. Hyper Strategy Logic
  9. Encoding SL$_{\mathit{ii}}$ Into HyperSL
  10. Injective Labeling and Action Recording
  11. Enforcing Imperfect Information
  12. The Translation
  13. Encoding Size
  14. Encoding HyperSL Into SL$_{\mathit{ii}}$
  15. Self-Composition
  16. ...and 11 more sections

Key Result

lemma 1

Given an SL$_{\mathit{ii}}$ MC instance $(\mathcal{G}, \{\sim_o\}_{o \in \mathit{Obs}}, {\varphi})$ there exists an effectively computable SL$_{\mathit{ii}}$ instance $(\mathcal{G}', \{\sim'_o\}_{o \in \mathit{Obs}}, {\varphi}')$ where (1)$\mathcal{G}'$ is IL and AR, and (2)$(\mathcal{G}, \{\sim_o\}

Theorems & Definitions (12)

  • definition 1
  • lemma 1
  • Theorem 1
  • lemma 2
  • definition 2
  • Example 1
  • Theorem 2
  • definition 2
  • lemma 2
  • proof
  • ...and 2 more