Rational synthesis and the suspect game
strategy logic games of the form
- E-Nash: \(\exists x_1 ... \exists x_n \flat(a_0, x_0) ...\flat(a_n, x_n)(\varphi_0 \land NE(\varphi_1, ... , \varphi_n))\)
- A-Nash: \( \forall x_1 ... \forall x_n \flat(a_0, x_0) ...\flat(a_n, x_n)(NE(\varphi_1, ... , \varphi_n) \to \varphi_0)\)
can be encoded into zero-sum 2-player games ("the suspect game").
now, you can add an agent to the game and have them play to ensure \(\vaprhi_0\) instead of to maximise a preference ordering:
- cooperative: \(\exists x_0 \exists x_1 ... \exists x_n \flat(a_0, x_0) ...\flat(a_n, x_n)\varphi_0 \land NE(\varphi_1, ... , \varphi_n)\)
non-cooperative: \(\forall x_0 \( \forall x_1 ... \forall x_n \flat(a_0, x_0) ...\flat(a_n, x_n)(NE(\varphi_1, ... , \varphi_n) \to \varphi_0)\)
and that's rational synthesis!
And it brings us back down to "merely" 2-EXPTIME!
These are mechanism enforcing players.
Originally encountered during formal verification of multi-agent systems lecture series at ESSLLI 2026 by Wojtech Jamroga and Catalin Dima (slides), for which my notes are pending publication.
Related: