As Soon as Possible but Rationally

TL;DR

This work analyzes the algorithmic complexity of rational verification and synthesis in multi-player weighted-graph games with quantitative reachability. It leverages a framework combining nondeterministic Mealy machines, product constructions, and Parikh automata to witness and certify rational responses, and introduces Lassos to finitely represent infinite behaviors. The authors provide tight complexity classifications across Pareto-optimal and Nash-rational settings, including PSPACE, NP, coNP, EXPTIME, and Π2P results, as well as hardness and containment results for one- and multi-player environments. The study clarifies when rational synthesis is tractable and identifies fundamental limits (e.g., undecidability with negative weights), offering a solid basis for future work on SPEs, stronger notions of equilibrium, and fixed-parameter tractability in rational verification and synthesis.

Abstract

This paper addresses complexity problems in rational verification and synthesis for multi-player games played on weighted graphs, where the objective of each player is to minimize the cost of reaching a specific set of target vertices. In these games, one player, referred to as the system, declares his strategy upfront. The other players, composing the environment, then rationally make their moves according to their objectives. The rational behavior of these responding players is captured through two models: they opt for strategies that either represent a Nash equilibrium or lead to a play with a Pareto-optimal cost tuple.

Figures (14)

• Figure 1: An example illustrating the two concepts of rational response.
• Figure 2: An example showing that PO lasso plays in the $\mathsf{coNCPV}$ problem may have an exponential length.
• Figure 3: Reduction from the countdown game problem to the $\mathsf{NCNS}$ problem (two-player env.).
• Figure 4: An arena with player $0$, player $\text{\scriptsize$\square$\normalsize}$, and player $\text{\large$\diamond$\normalsize}$, with no weight displayed.
• Figure 5: A nondeterministic Mealy machine of player $0$. The notation $v \mid v'$ on the transitions $(m,m')$ indicates that $m' \in \delta(m,v)$, and if $v \in V_0$, that $v' \in \tau(m,v)$, otherwise $v' = *$.

Theorems & Definitions (31)

• Example 3
• Theorem 4
• Theorem 5
• Theorem 6
• Lemma 8
• Example 9
• Proposition 10
• Proposition 11
• Lemma 12
• Lemma 13