{"id":"fd1cb010-a4e4-48c4-887f-9007be753abc","arxiv_id":"2501.03187","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A wrapper-based method verifies PCTL properties of turn-based multi-agent reinforcement learning policies via single-policy probabilistic model checking.","lead":"This paper shows how to check formal requirements of trained turn-based multi-agent reinforcement learning agents by combining their policies into a single verification model. It tests the approach on four game environments and reports efficiency gains over a naive monolithic baseline.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The load-bearing issue is the argmax proxy: all Table 1 probabilities describe the deterministic greedy policy, not the stochastic epsilon-greedy/softmax agents that were trained, so the 'verify TMARL agents' claim is unsupported unless deployment is explicitly greedy.","rationale":"The paper's core construction--a joint policy wrapper plus incremental construction of an induced DTMC--is sound for memoryless deterministic policies, and the authors transparently state the argmax restriction in the Limitations. I do not find an independent fatal formal bug: the turn feature is well defined, the DTMC is induced from the chosen policy, and the environment encodings are plausible. The reader's weakest assumption is also the most load-bearing concern: every reported PCTL value in Table 1 is computed on the deterministic argmax policy, whereas the trained agents use epsilon-greedy exploration and are described as probabilistic policies. Unless the intended artifact is explicitly the greedy evaluation of the agents, the verified probabilities do not describe the agents that a user would deploy. This is not resolved by noting that RL agents are often evaluated greedily, because the paper does not say that evaluation is greedy, and the Limitations frames the argmax choice as a method restriction. A single experiment replacing argmax with the actual action distribution would settle the magnitude of the discrepancy. The scalability comparison against 'naive monolithic' model checking is also questionable--it appears to compare fixed-policy verification with full-MDP or maximizing model checking--but that is a benchmark-design weakness rather than a soundness break, and it reinforces rather than changes the conditional verdict. Therefore I agree with the reader's CONDITIONAL assessment and recommend no verdict change: the paper should be revised to scope its claims to deterministic policies or to verify the stochastic policies directly.","tokens_in":10991,"tokens_out":6545,"duration_ms":66348,"concrete_test":"Re-run the Pokemon 5HP and useHeal20P1 checks on the published COOL-MC branch, but replace the argmax action selection with the actual trained policy's full action distribution (epsilon-greedy with the final epsilon, e.g., 0.1, and optionally 0.5 as used in training) and build the induced DTMC from that stochastic policy. Then compare P(F won1), P(F won2), and P(heal pot1 = 1 U heal pot1 = 0) with Table 1; if any probability shifts by more than a few percentage points, the verified numbers do not characterize the stochastic agents and the claims must be scoped to greedy deployment only.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central soundness gap is in Section 4, Limitations: 'Our method allows the model checking of probabilistic policies by always choosing the action with the highest probability at each state.' The trained agents use epsilon-greedy exploration (epsilon = 0.5, epsilon_min = 0.1) and their neural-network policies output action probabilities; the paper does not state that evaluation or deployment is deterministic. Every PCTL value in Table 1 is computed on the induced DTMC of the argmax policy. If the actual agent samples actions according to its learned distribution or epsilon-greedy mechanism, the verified probabilities can differ substantially from those reported. For example, a property reported as 0.0, such as usePoisons0HealP1, could become positive as soon as any non-greedy action can lead to a poison attempt. No abstraction, bound, or concentration argument connects the argmax DTMC result to the stochastic policy, so the verification results as presented do not characterize the trained agents' behavior. This is load-bearing because it affects every experimental result, not just one benchmark; the paper's abstract and conclusion claim verification of TMARL agents without scoping the claim to deterministic evaluation.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":11150,"tokens_out":5762,"duration_ms":54138,"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":[{"comment":"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":"Section 4 (Limitations), Section 5.1, Table 1"},{"comment":"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":"Section 5.2, first research question"},{"comment":"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.","section":"Section 5.2, MABP scalability experiment"}],"minor_comments":[{"comment":"There are typos in the keywords and abstract, including 'Che cking' and 'c ompliance'; these should be corrected.","section":"Keywords and abstract"},{"comment":"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":"Table 1"},{"comment":"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":"Section 5.1, Training details"},{"comment":"The text reports '51, 6547, 296 transitions'; the numeric formatting is inconsistent and should be corrected to a single comma-separated number.","section":"Section 5.1, Pokemon model size"},{"comment":"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.","section":"Section 4"},{"comment":"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.","section":"End of manuscript"}],"recommendation":"major_revision","confidential_remarks":"The paper extends the author's own COOL-MC tool, and the self-citation is appropriate, but the text should clarify the delta with Gross et al. 2022. The comparison baseline 'naive monolithic model checking' is weak; a comparison against PRISM-games or another turn-based stochastic game verifier would substantially strengthen the scalability claim. The deterministic-argmax issue is the main correctness concern and is fixable by scoping the claims or by adding an epsilon-aware analysis."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the paper is a modest, honest application of single-policy PCTL model checking to TMARL. The induced DTMC construction is sound for the deterministic argmax policy, but every result in Table 1 is about that proxy, not the stochastic epsilon-greedy agents that were trained, so the headline claim about verifying TMARL agents overreaches as written.\n\nWhat's genuinely new: it's the first to apply single-policy PCTL model checking to turn-based multi-agent RL, using a joint policy wrapper plus a turn feature to force the MDP into a single policy. That's a simple and useful trick. The model-checking algorithms themselves are standard, and the paper doesn't overclaim novelty. It also gets credit for stating its limitations explicitly: no reward operator, inactive-agent handling, fully-observed state, same action space. And it builds on the author's COOL-MC tool rather than reimplementing things.\n\nSoft spots, in proportion. The biggest is the argmax proxy. The trained agents are stochastic (epsilon starts at 0.5, decays to 0.1), and the paper never says deployment is deterministic. Section 4's limitation admits this: 'always choosing the action with the highest probability.' But the abstract and conclusion say 'verify TMARL agents' without scoping to greedy. A property like usePoisons0HealP1=0.0 could be positive if the agent ever samples a poison action. No bound or abstraction connects the argmax DTMC to the actual stochastic policy. This doesn't sink the method as a tool, but it does sink the claim as stated.\n\nSecond, the scalability claim rests on a strawman baseline: 'naive monolithic model checking.' No comparison to PRISM-games or statistical model checking of the actual policy. The method itself times out on the full Pokemon battle (24h), and the multi-agent scaling figure shows exponential time per state, which is a real limitation.\n\nThird, no artifacts. The GitHub link points to a branch, but no commit hash, no PRISM files, no trained models. Exact reproduction is impossible.\n\nThese are addressable. The core idea is sound and honestly presented; the limitations section is better than average. But the claims need scoping, the baseline needs to be fairer, and the artifacts need to be released.\n\nReader: someone working on verification of RL agents or game AI will find the joint-wrapper trick worth trying on small finite MDPs. I'd send it to peer review, with a note that the argmax-scoping issue needs a major revision, because the idea is plausible and the gap is clear.","headline":"Sound but over-scoped: verifies a deterministic argmax proxy of TMARL policies, not the stochastic agents that were trained.","tokens_in":11730,"tokens_out":3441,"would_cite":false,"duration_ms":31781,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["turn-based multi-agent reinforcement learning","model checking","PCTL","Markov decision process","induced DTMC","neural network policy verification","probabilistic formal verification","scalability"],"falsifier":"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.","tokens_in":10721,"feed_emoji":"🎮","tokens_out":6805,"duration_ms":58609,"temperature":0.7,"pith_summary":"The paper claims that trained turn-based multi-agent reinforcement learning (TMARL) agents can be formally verified against complex requirements by converting their joint policy into a single deterministic Markov chain and running probabilistic model checking on that chain. The key move is to treat all agents as one joint agent, add a turn feature to the environment state, and have a wrapper consult the correct agent's neural network at each step, always selecting the action with the highest probability. This yields a fully deterministic induced DTMC whose reachable states can be built on the fly, avoiding the full state space explosion that makes naive monolithic model checking infeasible. The reported experiments show that this construction verifies PCTL properties in Pokemon, multi-armed bandit, Tic-Tac-Toe, and Coin Collection environments, and that it scales to over 100 agents where monolithic model checking fails at 24.","feed_headline":"Multi-agent RL policies verified as a single Markov chain","feed_subtitle":"Trained agents collapse into one deterministic Markov chain, letting formal verification scale to 100+ agents.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Provides the COOL-MC tool that builds an induced DTMC incrementally for a single RL policy, which this paper extends to joint policies with multiple agents.","marker":"(Gross et al., 2022)"},{"why":"Supplies the on-the-fly incremental construction technique that makes the induced DTMC building efficient by expanding only reachable states.","marker":"(Cassez et al., 2005)"},{"why":"Defines the PRISM modeling language and tool, which the paper uses to model the TMARL environments as MDPs.","marker":"(Kwiatkowska et al., 2011)"},{"why":"Supplies the Storm model checker, which performs the actual PCTL model checking on the induced DTMC in the experiments.","marker":"(Hensel et al., 2022)"},{"why":"Introduces PCTL, the logic used to express the probabilistic properties that the method verifies.","marker":"(Hansson and Jonsson, 1994)"},{"why":"Provides the formal foundations of MDPs, DTMCs, and probabilistic model checking that the whole approach relies on.","marker":"(Baier and Katoen, 2008)"}],"fun_headline_variants":["RL agents verified at scale by collapsing to one Markov chain","Verifying 100+ multi-agent RL agents via a single DTMC","Model checking scales to 100+ agents by fixing RL policies","One deterministic Markov chain verifies 100+ RL agents"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Verified probabilities describe the deterministic highest-probability action at each state, not the stochastic sampling of the trained agents.","fun_headline_variants_meta":{"raw":{"variants":["RL agents verified at scale by collapsing to one Markov chain","Verifying 100+ multi-agent RL agents via a single DTMC","Model checking scales to 100+ agents by fixing RL policies","One deterministic Markov chain verifies 100+ RL agents"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000711,"raw_usage":{"total_tokens":3132,"prompt_tokens":806,"completion_tokens":2326,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":422,"completion_tokens_details":{"reasoning_tokens":2255}},"tokens_in":422,"tokens_out":2326,"duration_ms":14211,"temperature":1.0,"reasoning_tokens":2255,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:52:23.183103+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the COOL-MC tool that builds an induced DTMC incrementally for a single RL policy, which this paper extends to joint policies with multiple agents."},{"cited_title":"G., and Lime, D","cited_arxiv_id":null,"evidence_quote":"Supplies the on-the-fly incremental construction technique that makes the induced DTMC building efficient by expanding only reachable states."},{"cited_title":"Z., Norman, G., and Parker, D","cited_arxiv_id":null,"evidence_quote":"Defines the PRISM modeling language and tool, which the paper uses to model the TMARL environments as MDPs."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Storm model checker, which performs the actual PCTL model checking on the induced DTMC in the experiments."},{"cited_title":"and Jonsson, B","cited_arxiv_id":null,"evidence_quote":"Introduces PCTL, the logic used to express the probabilistic properties that the method verifies."},{"cited_title":"and Katoen, J","cited_arxiv_id":null,"evidence_quote":"Provides the formal foundations of MDPs, DTMCs, and probabilistic model checking that the whole approach relies on."}],"review_version":1}