Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesising Full-Information Protocols

Dietmar Berwanger, Laurent Doyen, Thomas Soullard

TL;DR

This paper studies synthesis in games with imperfect information under a model of full-information protocols (FIP), where a single active player may receive the entire history from passive observers when communication occurs. It develops a two-stage approach: first a generic reduction from imperfect-information games to perfect-information games, and then a concrete rectangular-morphism construction tailored to FIP that yields a finite-state abstraction of the information structure. The authors prove decidability and analyze complexity: the synthesis problem for FIP with $n$ observers is $(n+1)$-EXPTIME-complete, and the problem is non-elementary in general due to the growth of information; they also establish a strict expressiveness hierarchy with more observers, and show two-tape automata can express indistinguishability relations beyond FIP. These results provide a principled method to solve distributed reactive-system synthesis problems under maximal-information communication, clarifying the trade-offs between communication, information, and computational complexity in hierarchical information settings.

Abstract

We lay out a model of games with imperfect information that features explicit communication actions, by which the entire observation history of a player is revealed to another player. Such full-information protocols are common in asynchronous distributed systems; here, we consider a synchronous setting with a single active player who may communicate with multiple passive observers in an indeterminate environment. We present a procedure for solving the basic strategy-synthesis problem under regular winning conditions. We present our solution in an abstract framework of games with imperfect information and we split the proof in two conceptual parts: (i) a generic reduction schema from imperfect-information to perfect-information games, and (ii) a specific construction for full-information protocols that satisfies the requirement of the reduction schema. Furthermore we show that the number of passive observers induces a strict hierarchy, both in terms of expressiveness and complexity: with n observers, a full-information protocol can express indistinguishability relations (defining imperfect information for the player in the protocol) that are not expressible with n-1 observers, and the strategy-synthesis problem is (n+1)-EXPTIME-complete.

Synthesising Full-Information Protocols

TL;DR

This paper studies synthesis in games with imperfect information under a model of full-information protocols (FIP), where a single active player may receive the entire history from passive observers when communication occurs. It develops a two-stage approach: first a generic reduction from imperfect-information games to perfect-information games, and then a concrete rectangular-morphism construction tailored to FIP that yields a finite-state abstraction of the information structure. The authors prove decidability and analyze complexity: the synthesis problem for FIP with observers is -EXPTIME-complete, and the problem is non-elementary in general due to the growth of information; they also establish a strict expressiveness hierarchy with more observers, and show two-tape automata can express indistinguishability relations beyond FIP. These results provide a principled method to solve distributed reactive-system synthesis problems under maximal-information communication, clarifying the trade-offs between communication, information, and computational complexity in hierarchical information settings.

Abstract

We lay out a model of games with imperfect information that features explicit communication actions, by which the entire observation history of a player is revealed to another player. Such full-information protocols are common in asynchronous distributed systems; here, we consider a synchronous setting with a single active player who may communicate with multiple passive observers in an indeterminate environment. We present a procedure for solving the basic strategy-synthesis problem under regular winning conditions. We present our solution in an abstract framework of games with imperfect information and we split the proof in two conceptual parts: (i) a generic reduction schema from imperfect-information to perfect-information games, and (ii) a specific construction for full-information protocols that satisfies the requirement of the reduction schema. Furthermore we show that the number of passive observers induces a strict hierarchy, both in terms of expressiveness and complexity: with n observers, a full-information protocol can express indistinguishability relations (defining imperfect information for the player in the protocol) that are not expressible with n-1 observers, and the strategy-synthesis problem is (n+1)-EXPTIME-complete.
Paper Structure (13 sections, 13 theorems, 5 equations, 5 figures)

This paper contains 13 sections, 13 theorems, 5 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Basic Notions
  3. Repeated games with imperfect information
  4. Full-Information Protocols
  5. Graph Games and Morphisms
  6. Game graphs
  7. Information tree
  8. Bisimulation
  9. Rectangular morphisms
  10. Solving FIP Games
  11. Pre-processing
  12. A rectangular morphism for FIP games
  13. Expressiveness

Key Result

Lemma 1

For every game $\mathcal{G}$ with indistinguishability relation $\sim$, there is a bijection that maps every strategy $s$ in the information tree $\mathcal{U}(\mathcal{G})$ to an (information-consistent) strategy $\tilde{s}$ of the original game $\mathcal{G}$, such that $\tilde{s}(\tau) = s([\tau]_{

Figures (5)

  • Figure 1: View graphs (we omit all edges pointing backwards, correspond to looking into the past).
  • Figure 2: A configuration.
  • Figure 3: Lifting of the configuration of \ref{['fig:configuration']} after Player $0$ synchronises with Player $1$.
  • Figure 4: Lifting of the configuration of \ref{['fig:configuration']} after Player $0$ synchronises with Player $2$.
  • Figure :

Theorems & Definitions (21)

  • Lemma 1
  • proof
  • Lemma 2
  • Lemma 3
  • proof
  • Lemma 4
  • proof
  • Theorem 1
  • Lemma 5
  • Lemma 6
  • ...and 11 more