REVIEW 3 major objections 6 minor 47 references
Turn-based Multi-Agent Reinforcement Learning Model Checking
T0 review · 3 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash
Pith's one-line read This paper demonstrates a way to formally verify turn-based multi-agent reinforcement learning agents by building a single deterministic Markov chain from their trained policies and model checking PCTL properties on it, with experiments…
desk verdict Sound but over-scoped: verifies a deterministic argmax proxy of TMARL policies, not the stochastic agents that were trained. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the induced DTMC obtained by applying the joint policy to the MDP. The joint policy wrapper reads a turn feature from the current state, selects the appropriate agent policy, and returns the argmax action, so every reachable state has one deterministic successor distribution. The DTMC is constructed incrementally, expanding only states reachable under the joint policy, and PCTL model checking is then performed on it with the Storm engine. This construction replaces the multi-agent interaction with a single fully deterministic probabilistic process, which is what makes the verification tractable and scalable.
What would settle it
Simulate the deployed agents with their training-time stochastic action selection (e.g., epsilon-greedy with epsilon = 0.5) and estimate the probability of a PCTL property from many episodes; if the estimate deviates from the value computed on the argmax-induced DTMC by more than the simulation error, the verified numbers do not describe the agents as deployed.
Extended reading notes
Core claim
The central discovery is that a turn-based multi-agent reinforcement learning system can be verified by modeling the environment as a Markov decision process extended with a turn feature, then resolving all nondeterminism through a joint policy wrapper that queries each agent's trained neural network and picks its highest-probability action. Applying this joint policy to the MDP produces an induced DTMC in which every reachable state has exactly one outgoing transition, and PCTL properties such as reachability and ordering constraints are then checked with the Storm model checker on this DTMC. The method is shown to complete within seconds or minutes in four benchmark environments, and it scales to more than 100 agents in the multi-armed bandit setting, whereas monolithic model checking runs out of memory at 24 agents. The paper explicitly states that the verified probabilities describe the deterministic argmax policy, not the stochastic sampling used during training.
Load-bearing premise
Verified probabilities describe the deterministic highest-probability action at each state, not the stochastic sampling of the trained agents.
Editorial extensions
If this is right
- Developers can query exact probabilities for in-game events, such as a low-HP Pokemon using a heal pot with probability 0.65 or three coin-collecting agents colliding in 36% of runs, without simulating the whole game.
- The method sidesteps the state explosion of monolithic model checking by expanding only states reachable under the joint policy, making verification possible in environments like the Pokemon endgame where the monolithic MDP exceeds memory.
- The approach scales to more than 100 cooperating agents in the multi-armed bandit benchmark, while monolithic checking fails at 24 agents, and the reported bottleneck is the time to query neural-network actions, not the model size.
- Because the induced DTMC uses the highest-probability action at each state, the computed probabilities are guaranteed only for agents that deploy the deterministic argmax policy, not for agents that continue to sample stochastically.
Reading between the lines
- If the argmax proxy is accepted as the deployed policy, the same induced-DTMC construction could be reused for other single-policy analyses, such as expected-reward computation or strategy synthesis, without re-modeling the environment.
- The turn feature used to flatten a multi-agent game into an MDP is a generic encoding, suggesting that any turn-based game with fully observed states and shared action spaces can be lifted to this verification pipeline with similar effort.
- A natural extension, not explored in the paper, would be a bound on the error introduced by the argmax approximation based on the probability mass of the selected action; such a bound would turn the method into interval-valued guarantees for stochastic deployed policies.
- The reported action-querying bottleneck could likely be reduced by batching neural-network forward passes during DTMC construction, further pushing the agent-count limit.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a method for verifying trained turn-based multi-agent reinforcement learning (TMARL) agents against PCTL properties. The approach models the multi-agent system as a single MDP extended with a turn feature, wraps the individual agent policies into a joint policy, and constructs the DTMC induced by that joint policy using the COOL-MC tool. The induced DTMC is then checked with Storm. Experiments are reported for Pokemon, a multi-armed bandit problem, Tic-Tac-Toe, and a three-agent coin-collection game, with a comparison to what the paper calls naive monolithic model checking. The central claimed contributions are that the method can verify TMARL agents and scales better than naive monolithic model checking.
Significance. If the results are interpreted for the deterministic greedy policy that the method actually verifies, the paper describes a sound and potentially useful engineering integration: reachable-state construction of an induced DTMC for a fixed joint policy of trained neural-network agents, enabling explicit-state PCTL model checking in environments where full-MDP model checking is infeasible. The experiments give concrete evidence that this works on several benchmark environments and that the state-space reduction relative to the full MDP can be substantial. Strengths of the paper include the use of existing tools (COOL-MC, Storm, PRISM language), a public repository, and the absence of any parameter fitting to the verification queries, so there is no circularity in the reported probabilities. However, the paper's central claim is broader than what is verified: every reported PCTL value is computed on the argmax deterministic policy, while the trained agents are stochastic, so the claimed verification of the trained TMARL agents is not supported without an explicit deterministic-deployment assumption or an epsilon-aware analysis.
major comments (3)
- [Section 4 (Limitations), Section 5.1, Table 1] The object actually verified is the deterministic policy that always selects the action with highest probability, while the trained agents are stochastic: the experiments use epsilon-greedy with epsilon = 0.5 and epsilon_min = 0.1, and the neural-network policies output action probability distributions. The paper never states that evaluation or deployment uses greedy action selection. Consequently, every numeric result in Table 1 is a property of the argmax-induced DTMC, not of the trained stochastic policy. For example, the reported 0.0 for usePoisons0HealP1 can become positive as soon as an epsilon-greedy agent samples a non-greedy action that can lead to a poison attempt. The abstract and conclusion claim that the method verifies TMARL agents; this claim must either be restricted to deterministic greedy deployment or the method must provide a formal connection, such as an epsilon-aware model or probability bounds, between the induced DTMC and the stochastic policy. This issue is load-bearing because it affects every reported verification result.
- [Section 5.2, first research question] The scaling comparison against 'naive monolithic model checking' is not a like-for-like comparison. Monolithic model checking analyzes the full MDP, including nondeterminism and the possibility of Pmax/Pmin queries, whereas the proposed method constructs the DTMC induced by one fixed policy. The reported advantage therefore conflates the model-size reduction obtained by fixing a policy with an algorithmic scalability advantage. Moreover, in the Pokemon full-battle setting the paper states that naive monolithic model checking runs out of memory while the proposed method times out after 24 hours; that outcome does not support the 'scales better' claim. To substantiate the contribution, the comparison should be made against a baseline that also fixes a policy or against an abstraction that preserves the property in question, and the full-battle result should be presented as a timeout for both approaches.
- [Section 5.2, MABP scalability experiment] The text claims that the method verifies that 'agent 1 never uses the riskier bandit' and cites the property query lost1 in Table 1, but the property is P(F lost1), i.e., the probability that agent 1 loses. Losing is not the same as choosing the riskier bandit, and the query as stated does not refer to actions at all. Either the property label or the interpretation must be corrected, and the 'do the agents perform specific moves' question should be answered with properties that mention actions explicitly.
minor comments (6)
- [Keywords and abstract] There are typos in the keywords and abstract, including 'Che cking' and 'c ompliance'; these should be corrected.
- [Table 1] The row for 'Pokemon won1' shows 'T O' in every column without an explanation in the text; the caption states that T O means the query did not complete within 24 hours, but the row still needs a brief textual explanation, and the table layout should be cleaned up.
- [Section 5.1, Training details] All training results are reported for a single seed (128) with no variance information or repeated runs, so the reported agent rewards and the resulting policies are not established as typical for the training configuration.
- [Section 5.1, Pokemon model size] The text reports '51, 6547, 296 transitions'; the numeric formatting is inconsistent and should be corrected to a single comma-separated number.
- [Section 4] The phrase 'probabilistic policies' is used to describe the argmax method, but Definition 3.2 only introduces deterministic policies; the terminology should be aligned, and a formal definition of the verified policy (including tie-breaking) should be given.
- [End of manuscript] The final line 'This figure orcid.png is available in png format from http://arxiv.org/ps/2501.03187v1' appears to be a leftover LaTeX artifact and should be removed.
Circularity Check
No circularity: induced-DTMC construction and PCTL queries are standard; self-citation to COOL-MC is a tool pointer, not load-bearing.
full rationale
The paper's derivation chain is: train TMARL policies; wrap them into a joint policy; construct an induced DTMC by querying the argmax action per state; evaluate PCTL properties on that DTMC with Storm. Each step is definitional in the standard model-checking sense: the PCTL value is computed on the model being checked, not fed back into the policies. The only dependency on prior work by the same author is the COOL-MC tool (Gross et al., 2022), which is an existing GitHub-released artifact and is not used to justify the central mathematical claim; the experiments explicitly state that Storm is used for model checking. The limitation in Section 4 that probabilistic policies are checked by always choosing the highest-probability action is a disclosed abstraction: the reported probabilities describe the induced deterministic policy, not necessarily the stochastic sampling behavior of the trained agents. That is a correctness/validity gap, not a circular derivation, because the argmax model is not defined in terms of the PCTL results, nor are the PCTL results fitted parameters. No step reduces an equation to itself by construction, and no load-bearing self-citation chain forces the conclusions.
Assumptions & free parameters
assumptions (4)
- domain assumption Environments can be modeled as finite MDPs in the PRISM language.
- domain assumption The state is fully observable and includes a turn feature that determines the active agent.
- domain assumption The stochastic neural policy is approximated by the deterministic argmax policy, and the verification result holds for the latter.
- domain assumption PCTL properties without the reward operator are sufficient for the requirements of interest.
Cite this review
Pith. "Pith review of Turn-based Multi-Agent Reinforcement Learning Model Checking." pith.science (2026). https://pith.science/paper/77H536BV
@misc{pith2026250103187,
author = {Pith},
title = {Pith review of: Turn-based Multi-Agent Reinforcement Learning Model Checking},
year = {2026},
howpublished = {\url{https://pith.science/paper/77H536BV}},
note = {Machine review of arXiv:2501.03187}
}
read the original abstract
In this paper, we propose a novel approach for verifying the compliance of turn-based multi-agent reinforcement learning (TMARL) agents with complex requirements in stochastic multiplayer games. Our method overcomes the limitations of existing verification approaches, which are inadequate for dealing with TMARL agents and not scalable to large games with multiple agents. Our approach relies on tight integration of TMARL and a verification technique referred to as model checking. We demonstrate the effectiveness and scalability of our technique through experiments in different types of environments. Our experiments show that our method is suited to verify TMARL agents and scales better than naive monolithic model checking.
Figures
Figures from the paper (1 more)
Reference graph
Works this paper leans on
-
[1]
write newline
" write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 if FUNCTIO...
-
[2]
Abu Dalffa, M., Abu-Nasser, B. S., and Abu-Naser, S. S. (2019). Tic-tac-toe learning using artificial neural networks
work page 2019
-
[3]
Baier, C. and Katoen, J. (2008). Principles of model checking . MIT Press
work page 2008
-
[4]
Berner, C., Brockman, G., Chan, B., Cheung, V., Debiak, P., Dennison, C., Farhi, D., Fischer, Q., Hashme, S., Hesse, C., J \' o zefowicz, R., Gray, S., Olsson, C., Pachocki, J., Petrov, M., de Oliveira Pinto, H. P., Raiman, J., Salimans, T., Schlatter, J., Schneider, J., Sidor, S., Sutskever, I., Tang, J., Wolski, F., and Zhang, S. (2019). Dota 2 with lar...
arXiv 2019
-
[5]
Reinforcement Learning with Probabilistic Guarantees for Autonomous Driving
Bouton, M., Karlsson, J., Nakhaei, A., Fujimura, K., Kochenderfer, M. J., and Tumova, J. (2019). Reinforcement learning with probabilistic guarantees for autonomous driving. CoRR , abs/1904.07189
work page Pith review arXiv 2019
-
[6]
Cassez, F., David, A., Fleury, E., Larsen, K. G., and Lime, D. (2005). Efficient on-the-fly algorithms for the analysis of timed games. In CONCUR , volume 3653 of Lecture Notes in Computer Science , pages 66--80. Springer
work page 2005
-
[7]
A., Raskin, J., and Zikelic, D
Chatterjee, K., Novotn \' y , P., P \' e rez, G. A., Raskin, J., and Zikelic, D. (2017). Optimizing expectation with guarantees in pomdps. In AAAI , pages 3725--3732. AAAI Press
work page 2017
-
[8]
Courcoubetis, C. and Yannakakis, M. (1988). Verifying temporal properties of finite-state probabilistic programs. In FOCS , pages 338--345. IEEE Computer Society
work page 1988
Show all 47 references
-
[9]
and Yannakakis, M
Courcoubetis, C. and Yannakakis, M. (1995). The complexity of probabilistic verification. J. ACM , 42(4):857--907
1995
-
[10]
and Komeili, M
Davoodi, O. and Komeili, M. (2021). Feature-based interpretable reinforcement learning based on state-transition models. In SMC , pages 301--308. IEEE
2021
-
[11]
Even-Dar, E., Mannor, S., Mansour, Y., and Mahadevan, S. (2006). Action elimination and stopping conditions for the multi-armed bandit and reinforcement learning problems. Journal of machine learning research , 7(6)
2006
-
[12]
Freak, G. (1996). Pokemon series
1996
-
[13]
and Platzer, A
Fulton, N. and Platzer, A. (2019). Verifiably safe off-model reinforcement learning. In TACAS (1) , volume 11427 of Lecture Notes in Computer Science , pages 413--430. Springer
2019
-
[14]
Gross, D., Jansen, N., Junges, S., and P \'e rez, G. A. (2022). Cool-mc: A comprehensive tool for reinforcement learning and model checking. In SETTA . Springer
2022
-
[15]
M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., and Wojtczak, D
Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., and Wojtczak, D. (2019). Omega-regular objectives in model-free reinforcement learning. In TACAS (1) , volume 11427 of Lecture Notes in Computer Science , pages 395--412. Springer
2019
-
[16]
D., Miltersen, P
Hansen, T. D., Miltersen, P. B., and Zwick, U. (2013). Strategy iteration is strongly polynomial for 2-player turn-based stochastic games with a constant discount factor. J. ACM , 60(1):1:1--1:16
2013
-
[17]
and Jonsson, B
Hansson, H. and Jonsson, B. (1994). A logic for reasoning about time and reliability. Formal Aspects Comput. , 6(5):512--535
1994
-
[18]
Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., and Ruijters, E. (2019). The quantitative verification benchmark set. In TACAS (1) , volume 11427 of Lecture Notes in Computer Science , pages 344--350. Springer
2019
-
[19]
Hasanbeig, M., Kroening, D., and Abate, A. (2019). Towards verifiable and safe model-free reinforcement learning. In OVERLAY@AI*IA , volume 2509 of CEUR Workshop Proceedings , page 1. CEUR-WS.org
2019
-
[20]
Hasanbeig, M., Kroening, D., and Abate, A. (2020). Deep reinforcement learning with temporal logics. In FORMATS , volume 12288 of Lecture Notes in Computer Science , pages 1--22. Springer
2020
-
[21]
Hensel, C., Junges, S., Katoen, J., Quatmann, T., and Volk, M. (2022). The probabilistic model checker Storm . Int. J. Softw. Tools Technol. Transf. , 24(4):589--610
2022
-
[22]
Jin, P., Tian, J., Zhi, D., Wen, X., and Zhang, M. (2022). Trainify: A cegar-driven training and verification framework for safe deep reinforcement learning. In CAV (1) , volume 13371 of Lecture Notes in Computer Science , pages 193--218. Springer
2022
-
[23]
Jothimurugan, K., Bansal, S., Bastani, O., and Alur, R. (2022). Specification-guided learning of nash equilibria with high social welfare. In CAV (2) , volume 13372 of Lecture Notes in Computer Science , pages 343--363. Springer
2022
-
[24]
P., Littman, M
Kaelbling, L. P., Littman, M. L., and Moore, A. W. (1996). Reinforcement learning: A survey. Journal of artificial intelligence research , 4:237--285
1996
-
[25]
Y., Ribeiro, A., Bastani, O., and Kumar, V
Khan, A., Zhang, C., Li, S., Wu, J., Schlotfeldt, B., Tang, S. Y., Ribeiro, A., Bastani, O., and Kumar, V. (2019). Learning safe unlabeled multi-robot planning with motion constraints. In IROS , pages 7558--7565. IEEE
2019
-
[26]
Kucera, A. (2011). Turn-based stochastic games. In Lectures in Game Theory for Computer Scientists , pages 146--184. Cambridge University Press
2011
-
[27]
Kwiatkowska, M., Norman, G., and Parker, D. (2019). Verification and control of turn-based probabilistic real-time games. In The Art of Modelling Computational Systems , volume 11760 of Lecture Notes in Computer Science , pages 379--396. Springer
2019
-
[28]
Kwiatkowska, M., Norman, G., Parker, D., and Santos, G. (2022). Symbolic verification and strategy synthesis for turn-based stochastic games. CoRR , abs/2211.06141
2022 arXiv
-
[29]
Kwiatkowska, M., Parker, D., and Wiltsche, C. (2018). PRISM -games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. Int. J. Softw. Tools Technol. Transf. , 20(2):195--210
2018
-
[30]
Z., Norman, G., and Parker, D
Kwiatkowska, M. Z., Norman, G., and Parker, D. (2011). PRISM 4.0: Verification of probabilistic real-time systems. In CAV , volume 6806 of Lecture Notes in Computer Science , pages 585--591. Springer
2011
-
[31]
and Togelius, J
Lee, S. and Togelius, J. (2017). Showdown AI competition. In CIG , pages 191--198. IEEE
2017
-
[32]
Li, J., Zhou, Y., Ren, T., and Zhu, J. (2020). Exploration analysis in finite-horizon turn-based stochastic games. In UAI , volume 124 of Proceedings of Machine Learning Research , pages 201--210. AUAI Press
2020
-
[33]
L., Topcu, U., Fu, J., Isbell, C., Wen, M., and MacGlashan, J
Littman, M. L., Topcu, U., Fu, J., Isbell, C., Wen, M., and MacGlashan, J. (2017). Environment-independent task specifications via GLTL . CoRR, abs/1704.04341
2017 arXiv
-
[34]
Mnih, V., Kavukcuoglu, K., Silver, D., Graves, A., Antonoglou, I., Wierstra, D., and Riedmiller, M. A. (2013). Playing atari with deep reinforcement learning. CoRR , abs/1312.5602
2013 arXiv
-
[35]
Nam, S., Hsueh, C., and Ikeda, K. (2022). Generation of game stages with quality and diversity by reinforcement learning in turn-based RPG . IEEE Trans. Games , 14(3):488--501
2022
-
[36]
Pagalyte, E., Mancini, M., and Climent, L. (2020). Go with the flow: Reinforcement learning in turn-based battle video games. In IVA , pages 44:1--44:8. ACM
2020
-
[37]
Riley, J., Calinescu, R., Paterson, C., Kudenko, D., and Banks, A. (2021a). Reinforcement learning with quantitative verification for assured multi-agent policies. In 13th International Conference on Agents and Artificial Intelligence . York
2021
-
[38]
Riley, J., Calinescu, R., Paterson, C., Kudenko, D., and Banks, A. (2021b). Utilising assured multi-agent reinforcement learning within safety-critical scenarios. In KES , volume 192 of Procedia Computer Science , pages 1061--1070. Elsevier
2021
-
[39]
S., Coogan, S., Sastry, S
Sadigh, D., Kim, E. S., Coogan, S., Sastry, S. S., and Seshia, S. A. (2014). A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications. In CDC , pages 1091--1096. IEEE
2014
-
[40]
Shahrampour, S., Rakhlin, A., and Jadbabaie, A. (2017). Multi-armed bandits in multi-agent networks. In ICASSP , pages 2786--2790. IEEE
2017
-
[41]
Silver, D., Huang, A., Maddison, C. J., Guez, A., Sifre, L., van den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap, T. P., Leach, M., Kavukcuoglu, K., Graepel, T....
2016
-
[42]
Svelch, J. (2020). Should the monster play fair?: Reception of artificial intelligence in Alien: Isolation. Game Stud. , 20(2)
2020
-
[43]
a llstr \
Vamplew, P., Smith, B. J., K \" a llstr \" o m, J., de Oliveira Ramos, G., Radulescu, R., Roijers, D. M., Hayes, C. F., Heintz, F., Mannion, P., Libin, P. J. K., Dazeley, R., and Foale, C. (2022). Scalar reward is not enough: a response to silver, singh, precup and sutton (202...
2022
-
[44]
and Garc \' a - S \' a nchez, P
Videga \' n, S. and Garc \' a - S \' a nchez, P. (2021). Performance study of minimax and reinforcement learning agents playing the turn-based game iwoki. Appl. Artif. Intell. , 35(10):717--744
2021
-
[45]
Wang, Y., Roohi, N., West, M., Viswanathan, M., and Dullerud, G. E. (2020). Statistically model checking PCTL specifications on Markov decision processes via reinforcement learning. In CDC , pages 1392--1397. IEEE
2020
-
[46]
and Watson, I
Wender, S. and Watson, I. D. (2008). Using reinforcement learning for city site selection in the turn-based strategy game civilization IV . In CIG , pages 372--377. IEEE
2008
-
[47]
V., and Plaat, A
Wong, A., B \"a ck, T., Kononova, A. V., and Plaat, A. (2022). Deep multiagent reinforcement learning: Challenges and directions. Artificial Intelligence Review , pages 1--34
2022
Reviewed August 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.