Privacy-preserving Nash Equilibrium Synthesis with Partially Ordered Temporal Objectives

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.