Privacy-preserving Nash Equilibrium Synthesis with Partially Ordered Temporal Objectives

TL;DR

This work addresses privacy-preserving Nash equilibrium synthesis in two-player deterministic graph games where players hold private, partially ordered temporal-goal preferences. It introduces a privacy-aware communication protocol with a stopping rule, formalizes a terminating product game ${H}_{ au}$, and reduces NE synthesis to Büchi-game constructions with nominal paths and punishment strategies. The authors establish completeness and privacy guarantees, propose GenKPrefs to generate privacy-preserving preorders, and validate the approach through a package-delivery scenario showing non-trivial equilibria can be achieved without exposing private preferences. The results demonstrate that privacy-conscious equilibrium synthesis is feasible in settings with limited information sharing, with practical implications for strategy synthesis in healthcare, logistics, and competitive domains.

Abstract

Nash equilibrium is a central solution concept for reasoning about self-interested agents. We address the problem of synthesizing Nash equilibria in two-player deterministic games on graphs, where players have private, partially-ordered preferences over temporal goals. Unlike prior work, which assumes preferences are common knowledge, we develop a communication protocol for equilibrium synthesis in settings where players' preferences are private information. In the protocol, players communicate to synthesize equilibria by exchanging information about when they can force desirable outcomes. We incorporate privacy by ensuring the protocol stops before enough information is revealed to expose a player's preferences. We prove completeness by showing that, when no player halts communication, the protocol either returns an equilibrium or certifies that none exists. We then prove privacy by showing that, with stopping, the messages a player sends are always consistent with multiple possible preferences and thus do not reveal some given secret regarding a player's true preference ordering. Experiments demonstrate that we can synthesize non-trivial equilibria while preserving privacy of preferences, highlighting the protocol's potential for applications in strategy synthesis with constrained information sharing.

Figures (4)

• Figure 1: A semi-automaton over atomic propositions $\{\alpha,\beta\}$ that encodes if some event $\alpha$ occurs before some $\beta$.
• Figure 2: A game, adapted from bouyer2016stochastic, where proper strategies induce interesting equilibrium properties. Player 1's states are circles, player 2's states are squares, and actions are transition annotations. The initial node is $(a,0)$. We set $L(a) = \alpha$ and $L(b) = \beta$. The semi-automaton $\langle \{q_1,q_2\},\{\alpha,\beta\},\delta, q_1 \rangle$ tracks the last node, i.e., $\delta(\cdot, \alpha) = q_1$ and $\delta(\cdot,\beta) = q_2$. Each player prefers not to be the one terminating the game, i.e., $q_2 \succ_{E_1} q_1$ and $q_1 \succ_{E_2} q_2$.
• Figure 3: An example environment. Gray nodes are in $\mathcal{D}$, and the initial node is orange. The left graph is $(\mathcal{T},\mathcal{F}_1)$, and the right graph is $(\mathcal{T},\mathcal{F}_2)$
• Figure 4: (a) Nominal paths of NE strategies in the game in Figure \ref{['fig:envExample']}. A blue and red edge indicates that players $1$ and $2$ are in control respectively. (b,c) Preorders $E_1 \in \mathfrak{U}$ and $\tilde{E}_1 \in \mathfrak{U}^c$ for player 1 that produce the same query responses. These preorders satisfy $\{v\}^\uparrow_{E_1} = \{v\}^\uparrow_{\tilde{E}_1}$ for $v$ in $\{\top,b,d\}$.

Theorems & Definitions (39)

• Definition 1
• Definition 2
• Proposition 1
• Definition 3
• Definition 4
• Example 1
• Definition 5
• Definition 6
• Definition 7
• Remark 1