Most General Winning Secure Equilibria Synthesis in Graph Games

Abstract

Abstract This paper considers the problem of co-synthesis in k-player games over a finite graph where each player has an individual $$\omega $$ ω -regular specification $$\phi _i$$ ϕ i . In this context, a secure equilibrium (SE) is a Nash equilibrium w.r.t. the lexicographically ordered objectives of each player to first satisfy their own specification, and second, to falsify other players’ specifications. A winning secure equilibrium (WSE) is an SE strategy profile $$(\pi _i)_{i\in [1;k]}$$ ( π i ) i ∈ [ 1 ; k ] that ensures the specification $$\phi :=\bigwedge _{i\in [1;k]}\phi _i$$ ϕ : = ⋀ i ∈ [ 1 ; k ] ϕ i if no player deviates from their strategy $$\pi _i$$ π i . Distributed implementations generated from a WSE make components act rationally by ensuring that a deviation from the WSE strategy profile is immediately punished by a retaliating strategy that makes the involved players lose. In this paper, we move from deviation punishment in WSE-based implementations to a distributed, assume-guarantee based realization of WSE. This shift is obtained by generalizing WSE from strategy profiles to specification profiles $$(\varphi _i)_{i\in [1;k]}$$ ( φ i ) i ∈ [ 1 ; k ] with $$\bigwedge _{i\in [1;k]}\varphi _i = \phi $$ ⋀ i ∈ [ 1 ; k ] φ i = ϕ , which we call most general winning secure equilibria (GWSE). Such GWSE have the property that each player can individually pick a strategy $$\pi _i$$ π i winning for $$\varphi _i$$ φ i (against all other players) and all resulting strategy profiles $$(\pi _i)_{i\in [1;k]}$$ ( π i ) i ∈ [ 1 ; k ] are guaranteed to be a WSE. The obtained flexibility in players’ strategy choices can be utilized for robustness and adaptability of local implementations. Concretely, our contribution is three-fold: (1) we formalize GWSE for k-player games over finite graphs, where each player has an $$\omega $$ ω -regular specification $$\phi _i$$ ϕ i ; (2) we devise an iterative semi-algorithm for GWSE synthesis in such games, and (3) obtain an exponential-time algorithm for GWSE synthesis with parity specifications $$\phi _i$$ ϕ i .