We study rational synthesis for stochastic multi-agent systems with unknown dynamics, where each agent is equipped with its own probabilistic temporal objective specified using Probabilistic Linear Temporal Logic on Finite Traces (\mathsf{PLTL}_f}). We impose solution concepts (e.g., Nash equilibrium, subgame-perfect equilibrium) as constraints on the joint strategy profile, using payoffs derived from each agent's probability of satisfying its temporal objective. In particular, we formulate per-agent rational synthesis as finding a strategy profile -- if one exists -- such that (i) the designated agent's probabilistic temporal constraint is satisfied, and (ii) the profile represents a stable solution under a chosen solution concept. We give conditional convergence guarantees for tabular Nash-Q learning, certify satisfaction with simultaneous finite-sample confidence bounds, and assess strategic stability with approximate best-response checking. Our approach operates in a stochastic Multi-Agent Reinforcement Learning (MARL) environment, where model-free learning algorithms attempt to attain extremal satisfaction probabilities for temporal objectives automatically compiled into reward automata. Our approach is empirically validated using 8 general-sum concurrent stochastic games.
Figures & tables
Figure 1. DFA for F(intruder_breach)∧G(¬collision) in Stochastic Pursuit Evasion . State 0 is initial and state 2 is accepting. Acceptance is evaluated at episode end. Three-state reward automaton. State 0 waits for an intruder breach without collision, state 2 records success, and any collision leads to the absorbing failure state 1.
Figure 2. Best-agent satisfaction of each family’s stronger variant, with or without CER (mean and 95% CIs over five runs). Diamonds mark the strongest handcrafted-reward baseline’s separately evaluated final satisfaction at its final training step. Eight panels compare best-agent satisfaction over training across the benchmarks. Bands show confidence intervals, and diamonds mark handcrafted-reward baselines.
Appendix figures & tables11 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 3. Overview of our approach to automata-based rational synthesis. Temporal objectives are compiled into reward automata and combined with the game. Model-free learners, optionally using counterfactual replay, produce a profile evaluated for satisfaction and strategic stability.
Figure 4. The four spatial environment families used in our experiments. Spatial layouts for Pursuit-Evasion, Coins, Territory, and Commons Harvest.
Figure 5. Stage payoff matrix for Matrix Stag Hunt . The ordered pair in each cell gives the payoff to Player 1 and Player 2, respectively. Rows and columns are Hare and Stag for Players 1 and 2. The payoffs are (3,3), (3,0), (0,3), and (4,4), respectively.
Figure 6. Two-player Pursuit Classic: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for each Pursuit-Evasion role, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 7. Two-player Pursuit Capture: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for each Pursuit-Evasion role, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 8. Three-player Pursuit Classic: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for each Pursuit-Evasion role, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 9. Three-player Pursuit Capture: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for each Pursuit-Evasion role, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 10. Coins: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Per-agent learning curves for both Coins players, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 11. Matrix Stag Hunt: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for both Stag Hunt players, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 12. Commons Harvest: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for the four Commons Harvest agents, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Figure 13. Territory: per-agent satisfaction (mean and 95% CIs over five seeds). Left: best variant per learner family; right: all objective-trained variants. Learning curves for both Territory competitors, comparing the best-performing algorithms on the left and all evaluated algorithms on the right, with confidence bands.
Reinforcement learning studies how agents learn sequential decisions from rewards and interaction, balancing exploration, performance, safety, and adaptation.
Reasoning about what agents can achieve through strategic interaction is a core challenge in Multi-Agent Systems (MAS). Logics for strategic ability, such as ATL, provide rigorous methods, but their adoption is often hindered by the computational cost of strategy synthesis. We introduce a neuro-symbolic framework that integrates large language models (LLMs) into the model-checking pipeline for MAS. The LLM acts as a strategy-generation oracle, proposing candidate strategies that are then formally validated by a standard MAS model checker. This generate-and-certify architecture uses LLM guidance to navigate large combinatorial strategy spaces while preserving formal soundness: generated strategies are accepted only when certified by the verifier. We instantiate the framework for bounded strategic reasoning in NatATL and introduce the first NatATL strategy-synthesis dataset, consisting of 4211 instances. Experiments with an open-weight Qwen3-32B model show that our certified pipeline achieves 92% accuracy on strategy-synthesis outcomes.
Marco Aruta, Vadim Malvone, Aniello Murano +2
University of Naples Federico II, Naples, Italy · LTCI, Télécom Paris, Institut Polytechnique de Paris, Palaiseau, France · Università degli Studi di Salerno, Salerno, Italy
Provably efficient and robust equilibrium computation in general-sum Markov games remains a core challenge in multi-agent reinforcement learning. Nash equilibrium is computationally intractable in general and brittle due to equilibrium multiplicity and sensitivity to approximation error. We study Risk-Sensitive Quantal Response Equilibrium (RQRE), which yields a unique, smooth solution under bounded rationality and risk sensitivity. We propose RQRE-OVI, an optimistic value iteration algorithm for computing RQRE with linear function approximation in large or continuous state spaces. Through finite-sample regret analysis, we establish convergence and explicitly characterize how sample complexity scales with rationality and risk-sensitivity parameters. The regret bounds reveal a quantitative tradeoff: increasing rationality tightens regret, while risk sensitivity induces regularization that enhances stability and robustness. This exposes a Pareto frontier between expected performance and robustness, with Nash recovered in the limit of perfect rationality and risk neutrality. We further show that the RQRE policy map is Lipschitz continuous in estimated payoffs, unlike Nash, and RQRE admits a distributionally robust optimization interpretation. Empirically, we demonstrate that RQRE-OVI achieves competitive performance under self-play while producing substantially more robust behavior under cross-play compared to Nash-based approaches. These results suggest RQRE-OVI offers a principled, scalable, and tunable path for equilibrium learning with improved robustness and generalization.
Jake Gonzales, Max Horwitz, Eric Mazumdar +1
Department of Electrical & Computer Engineering, University of Washington · Computing & Mathematical Sciences, California Institute of Technology
Responsibility allocation -- determining the extent to which agents are accountable for outcomes -- is a fundamental challenge in the design and analysis of multi-agent systems. In this work, we model such systems as concurrent stochastic multi-player games and introduce a notion of retrospective (backward) counterfactual responsibility, which quantifies an agent's accountability for outcomes resulting from a given strategy profile. To allocate responsibility among agents, we utilise the Shapley value and formally show that this method satisfies key desirable properties, including fairness and consistency. Building on this foundation, we propose a formal framework that supports both verification and strategic reasoning in responsibility-aware multi-agent systems. Furthermore, by adopting Nash equilibrium as the solution concept, we demonstrate how to compute stable strategy profiles in which agents trade off responsibility against expected reward.