{"id":"dca67db4-79e8-4bcf-b54d-98867339f3e6","arxiv_id":"2506.01010","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Converting concurrent game frames to effectivity frames can drastically speed up alternating-time mu-calculus model checking on games where many joint moves are equivalent, at the cost of a one-time conversion that is not always recouped.","lead":"The paper implements model checking for the alternating-time mu-calculus (AMC) using both the standard concurrent-game representation and the more compact effectivity-frame representation, and measures when converting between them pays off. Its experiments show large speedups on games where many different move combinations have the same effect, but the conversion cost can outweigh the benefit in other settings.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Amortized CGF-to-EF conversion is asserted but not measured; the abstract's 'often outweighed' claim rests on a multi-formula reuse scenario that no experiment in the paper actually runs.","rationale":"The reader's weakest assumption — that CGF-to-EF conversion amortizes over repeated modal evaluation — is indeed the load-bearing condition for the abstract's claim. I agree with the reader's diagnosis, with one refinement: the critical repetition is not merely 'modalities evaluated repeatedly at the same state within a single fixpoint computation'; the experiments already exercise that internally. The decisive, unmeasured repetition is across multiple formulas or multiple model checking runs on the same model, since the conversion is done once per model and its cost is plotted as a one-time overhead in single-formula figures. The paper's own castle-game results contradict 'often outweighed' for that regime, and the modulo game's tiny 10-state size undermines the 'large systems' phrasing. The correctness machinery — Definition 1, Lemmas 2 and 9, the parity-game reductions, and the COOL-MC implementations — appears sound, and the comparison with MCMAS is useful evidence of the tool's practical behavior. The hedged 'first full-AMC model checker' claim is plausible but not independently verified. These issues are addressable by an additional benchmark and a more carefully scoped abstract, so CONDITIONAL is the appropriate verdict rather than rejection.","tokens_in":14732,"tokens_out":1948,"duration_ms":22270,"concrete_test":"Run a multi-formula amortization benchmark on both the castle game (4--10 castles, health 2--10) and the modulo game (base 10, 2--10 moves/agent, 2--5 agents): for each fixed model instance, evaluate K = 10, 50, 200 distinct AMC formulas (or K random formulas of size 64) on the same CGF, and compare total runtime for CGFg/CGFl versus EFCg/EFCl with the conversion performed exactly once. If EFC variants never beat CGF variants even at K = 200 on the castle game, then 'often outweighed' is false for systems without many equivalent moves; if they do win, report the crossover K and reword the claim to state the required number of formulas per model.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The abstract's empirical claim ('on large systems, the overhead involved in converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking') is the paper's headline contribution. It requires that conversion cost be amortized across repeated model checking of the same CGF. However, no experiment measures this amortization: Fig. 2 explicitly reports 'mean cumulative runtime including model conversion time for one run' on one random formula per model; Figs. 4--6 each evaluate a single formula family. The castle game, the paper's large-system benchmark, shows that 'the cost of conversion outweighs this speedup at this model size' (§5.4), and the modulo game, where EF wins, has only 10 states and conversion time grows as moves_per_agent^|Ag| (Fig. 3). The only support for amortization is the speculative remark that 'if a large number of formulas is to be evaluated on the same model, the cost of conversion is expected to amortize' — not a measurement. Moreover, §6 proposes by-need conversion as future work, which is exactly the feature that would make the conversion less costly. The theoretical contributions, the translation implementation, and the correctness lemmas are sound as far as I can see, but the central performance claim is under-supported as written.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents an implementation of model checking for the alternating-time mu-calculus (AMC) on concurrent game frames (CGFs) and on effectivity frames (EFs), including a translation from CGFs to EFs. The algorithms are realized as instantiations of the COOL-MC framework, using both parity-game reduction and a local fixpoint method. Experiments on random models, the castle game, and a modulo game compare CGF-based and EF-based checking with each other and, on the ATL fragment, with MCMAS. The paper claims in the abstract that on large systems the overhead of converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking, and that this is the first model checker covering the full AMC.","tokens_in":14869,"tokens_out":6080,"duration_ms":63020,"significance":"The theoretical core is sound and cleanly presented: Lemma 2 proves the semantic equivalence of a CGF and its induced effectivity frame, and Lemma 9 and Corollary 6 provide the correctness statements for the model-checking algorithms. The implementation and artifact are a genuine contribution, and the benchmark design includes a deliberately constructed modulo game that isolates the effect of many equivalent joint moves. The comparison with MCMAS is appropriately caveated as explicit-state versus symbolic. However, the paper's headline empirical claim about amortized conversion costs is not directly supported by the experiments as reported, and the runtime data lack variance information. If the central claim is retained, it needs additional experiments or a substantial qualification.","major_comments":[{"comment":"The abstract's claim that on large systems the overhead of converting a CGF to an effectivity frame is 'often outweighed' by subsequent model-checking benefits is not established by the reported experiments. Figures 4–6 evaluate single formula families, and Fig. 2 reports one random formula per model; no experiment checks multiple formulas against the same converted EF, which is exactly the amortization scenario needed to support the claim. Section 5.4 itself states for the castle game that 'the cost of conversion outweighs this speedup at this model size' and only says that amortization is 'expected', not measured. Please either add a multi-formula benchmark that measures total runtime with and without a single conversion, or weaken the abstract and conclusion to claim a benefit only when the input is already an EF or when many modal evaluations are performed on a per-state basis.","section":"Abstract and §5.4"},{"comment":"The runtime plots report only mean values, with no standard deviations, confidence intervals, or per-instance data. The statement that 'spikes in the plots appear to be due to symmetry' in Section 5.4 is a conjecture with no supporting measurement. Because the paper's central claim is comparative and quantitative, the absence of variance information makes it impossible to judge whether the reported crossings and speedups, such as the break-even point near formula size 16 in Fig. 2, are robust across instances.","section":"§5.4 and Figs. 2–6"},{"comment":"The conversion-time scaling in the modulo game is exponential in the number of agents, as noted in Section 5.4, and the modulo game has only 10 states. The castle game is run with 4 castles, so the conclusion that EF-based checking wins on 'large systems' is not demonstrated at the scale where the amortization argument would be most relevant. Please report experiments with larger state spaces and more agents, or restrict the claim to systems with many equivalent joint moves and to the per-formula speedup after conversion.","section":"§5.4 and Fig. 3"}],"minor_comments":[{"comment":"The code listings contain ellipses and omit definitions of several identifiers, including d, d_bar, next_move_for, and the hash-table operations; please add enough context or a pointer to the artifact so the reader can follow the implementation.","section":"§4.4, Listings 1–3"},{"comment":"The random benchmark description should specify the distribution over formulas and models, including how propositional atoms, modalities, and fixpoint alternations are sampled, and how many formulas are generated per size; otherwise Fig. 2 is difficult to interpret.","section":"§5.1"},{"comment":"The formula phi2 is stated as expressing a Büchi property, but the paper does not justify this reading; a one-sentence explanation of why the nested fixpoint enforces infinitely many visits to p0 and p_{base/2} would help.","section":"§5.3"},{"comment":"The sentence 'The castle game ... which are expressible in ATL' should be clarified: the properties are ATL-definable, but the formulas are written in AMC syntax; the current wording is slightly ambiguous.","section":"§5.4"},{"comment":"The caption of Fig. 2 says 'mean cumulative runtime including model conversion time for one run', but it is not clear whether the conversion is included once per formula or once per model; please clarify, and also state the number of states and agents in the random models.","section":"§5.4 and Fig. 2"},{"comment":"The artifact is described as 'will be made available', while the arXiv header says artifacts are available and evaluated; please include a persistent artifact DOI or a direct link in the paper, and add the version number for hyperfine in reference [21].","section":"References and artifact"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope for a verification/tools venue, and the theoretical and implementation contributions are solid. The main risk is that the abstract overstates the experimental support for the amortization claim. If the authors cannot supply a multi-formula amortization experiment, the editor should insist on a qualified abstract and conclusion. The 'first full AMC model checker' claim is plausible but should be checked against recent tool surveys and stated with the 'to our knowledge' caveat in all occurrences."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read the Hausmann et al. paper on AMC model checking via effectivity frames. Here is my take.\n\nWhat is actually new: an implementation of the known CGF-to-effectivity-frame translation inside COOL-MC, instantiated for both semantics, plus the first (as far as they know) model checker covering the full AMC. The semantic equivalence (Lemma 2) is standard but cleanly proved, and the parity-game and local-model-checking reductions are spelled out carefully. The benchmark suite is reasonably broad: random formulas, castle game, modulo game, and a comparison to MCMAS on ATL. The theoretical claims are sound.\n\nWhere it gets soft. The abstract's headline claim - that on large systems the conversion overhead is 'often outweighed' by subsequent model-checking benefits - is not established by the experiments. The conversion is a one-time cost, and the paper's own justification is that, especially in AMC, modalities may be evaluated repeatedly at the same state. But no experiment actually runs multiple formulas on the same converted EF to test amortization. Instead, each benchmark evaluates a single formula (or formula family) on each model, with conversion time included. The castle game, their large-system benchmark, shows conversion cost exceeding the EF speedup at those sizes; the modulo game, where EF wins, has only 10 states and conversion cost grows as moves_per_agent^|Ag|. The 'spikes due to symmetry' explanation needs support. And the artifact is promised but not yet available at time of reading, despite the 'Artifacts Available' badge in the header - a discrepancy worth flagging.\n\nNone of this breaks the core theoretical contribution or the engineering value. The paper would be stronger if it either (a) ran a proper amortization experiment (several formulas, measure total time with and without conversion), or (b) softened the abstract claim to match the data, e.g. 'can be outweighed on systems with many equivalent joint moves.'\n\nVerdict: worth serious refereeing. The implementation is real, the claims are checkable, and the benchmark infrastructure is reusable. The empirical overreach is fixable with additional experiments or rephrasing. I would send it to a reviewer familiar with both ATL semantics and tool benchmarking.","headline":"Solid implementation and sound theory, but the abstract overstates the empirical case: the amortization that would justify CGF-to-EF conversion is never actually measured.","tokens_in":15493,"tokens_out":2593,"would_cite":true,"duration_ms":25734,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","68Q60","91A80"],"pacs":[],"model":"deepseek-v4-flash","headline":"Converting concurrent game frames to effectivity frames makes AMC model checking faster on large systems.","keywords":["alternating-time mu-calculus","ATL","effectivity frames","concurrent game frames","model checking","multi-agent systems","coalitional modalities","parity games"],"falsifier":"Run the local checker on large random concurrent game frames against a formula that asks a single non-nested coalitional ability query, and compare end-to-end direct checking with convert-then-check on an effectivity frame. Since no fixpoint re-evaluates the modality at the same state, the effectivity-frame pipeline should lose by at least the measured conversion time; if it does not, the amortization explanation is not what drives the reported speedups.","tokens_in":1561,"feed_emoji":"🎮","tokens_out":6091,"duration_ms":154385,"temperature":0.7,"pith_summary":"The paper tries to establish that model checking for the alternating-time mu-calculus (AMC), a fixpoint logic for what groups of agents can force in a multi-agent game, is faster in practice when the input game is first rewritten into an effectivity frame, a structure that records which sets of states each coalition can force next. In a concurrent game frame, a single coalitional modality means nested quantifiers over joint moves, which grows expensive as the number of agents increases; on an effectivity frame, the same modality becomes a lookup and a set-containment test. The paper argues that the one-time rewrite pays for itself on large systems because coalitional modalities are evaluated repeatedly at the same state while AMC formulas are checked, and the experiments on random games and two benchmark families are consistent with that trade-off. The paper also reports the first model checker that covers the full AMC, which contains ATL*, rather than only the ATL fragment.","feed_headline":"Convert the game once, then check strategic ability fast","feed_subtitle":"A one-time rewrite into effectivity frames pays off on large multi-agent systems and enables full-AMC checking.","key_machinery":"The load-bearing object is the induced effectivity frame of Definition 1: from a concurrent game frame one computes, at each state and for each coalition, the collection of outcome sets that the coalition can force against any play of the complementary coalition; the paper keeps only the minimal sets and stores them in a lookup table. The identity carrying the argument is Lemma 2, which equates the two semantics for every AMC formula: on an effectivity frame, a coalitional modality $[C]\\psi$ is true exactly when some enforceable set is contained in the current extension of $\\psi$, and $\\langle C\\rangle\\psi$ exactly when every enforceable set intersects that extension. This replaces the nested existential-universal quantifiers over joint moves with one set-containment test per evaluation.","core_discovery":"The central claim is that effectivity frames are not merely an equivalent semantics for AMC but a practical route to faster checking: translating a concurrent game frame into an effectivity frame moves the expensive coalitional quantifier alternation into a per-state precomputation, so that a later check of $[C]\\psi$ only asks whether some enforceable set is contained in the current extension of $\\psi$, and $\\langle C\\rangle\\psi$ only asks whether every enforceable set meets that extension. The paper proves the equivalence of the two semantics, instantiates both a parity-game-based algorithm and a local fixpoint-iteration algorithm on both representations, and measures where the trade-off lands. It finds that the effectivity-frame route wins clearly when the game has many equivalent joint moves, overtakes direct concurrent-game checking on large random formulas past a break-even point, and is dominated by conversion overhead on small models; against a symbolic ATL checker, it wins on systems that lack succinct symbolic encodings and loses on systems with almost no equivalent joint moves.","pith_inferences":["The amortization argument implies a clean engineering rule the paper does not state: prefer conversion for fixpoint-heavy formulas where ability questions recur at the same state, and skip it for one-shot ATL-style checks.","Adding aggressive caching of coalitional-modality results or bisimulation-style quotienting to a concurrent-game checker could erase much of the effectivity-frame advantage, because both reduce the repeated evaluations the amortization depends on.","The same rewrite should transfer to other logics over concurrent games whose semantic core is a per-state coalitional power relation, such as fragments of strategy logic, although the paper does not test that."],"forward_implications":["On systems with many equivalent joint moves, effectivity-frame checking keeps runtime roughly constant as the number of moves per agent grows, while direct concurrent-game checking slows down sharply.","For large random formulas, converting first and then checking overtakes direct checking once formula size passes the observed break-even point, which the local variant reaches at around sixteen connectives in the reported experiments.","The implementation is the first model checker for the full AMC, so AMC-only specifications such as Büchi-style coalitional objectives can be checked, not just ATL.","Because the conversion is per-state, it can be parallelized, and converting only when a modality is first evaluated would reduce the small-model penalty.","Systems already presented as effectivity frames can be checked directly without any conversion cost."],"supporting_citations":[{"why":"It defines alternating-time temporal logic and its fixpoint extension over concurrent game frames, the standard semantics the paper starts from.","marker":"[2]"},{"why":"It introduces effectivity frames and playability, the alternative semantics whose computational benefits the paper tests.","marker":"[20]"},{"why":"It provides the generic game-based local model checking algorithm that the paper instantiates for both CGF and effectivity-frame semantics.","marker":"[11]"},{"why":"It compares concurrent game frames, effectivity frames, and alternating transition systems, supporting the equivalence and playability background.","marker":"[6]"},{"why":"It supplies the state-of-the-art ATL model checker used as the external baseline in the benchmark comparison.","marker":"[17]"},{"why":"It provides the parity-game solver used by the game-based model checking variants.","marker":"[24]"},{"why":"It describes the generic model-checking environment in which both semantics are implemented.","marker":"[10]"}],"fun_headline_variants":["Effectivity frames speed up AMC model checking on large systems","One-time conversion pays off for large strategic model checks","Convert game frames to effectivity for faster AMC checking","Effectivity translation beats direct checking on big games","Precompute effectivity to accelerate alternating-time checks"],"cache_read_input_tokens":17536,"weakest_assumption_plain":"The speedup rests on the premise that ability questions of the form 'can this group force that outcome?' are asked repeatedly at the same state during a check; if each such question is asked only once, the one-time game rewrite is pure overhead and direct checking should win.","fun_headline_variants_meta":{"raw":{"variants":["Effectivity frames speed up AMC model checking on large systems","One-time conversion pays off for large strategic model checks","Convert game frames to effectivity for faster AMC checking","Effectivity translation beats direct checking on big games","Precompute effectivity to accelerate alternating-time checks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00028,"raw_usage":{"total_tokens":1662,"prompt_tokens":949,"completion_tokens":713,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":565,"completion_tokens_details":{"reasoning_tokens":636}},"tokens_in":565,"tokens_out":713,"duration_ms":7280,"temperature":1.0,"reasoning_tokens":636,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:53:07.031694+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the local checker on large random concurrent game frames against a formula that asks a single non-nested coalitional ability query, and compare end-to-end direct checking with convert-then-check on an effectivity frame. Since no fixpoint re-evaluates the modality at the same state, the effectivity-frame pipeline should lose by at least the measured conversion time; if it does not, the amortization explanation is not what drives the reported speedups.","supporting_citations":[{"cited_title":"In: Concurrency Theory, CONCUR 2019","cited_arxiv_id":null,"evidence_quote":"It provides the generic game-based local model checking algorithm that the paper instantiates for both CGF and effectivity-frame semantics."},{"cited_title":"Information, Interaction and Agency pp","cited_arxiv_id":null,"evidence_quote":"It compares concurrent game frames, effectivity frames, and alternating transition systems, supporting the equivalence and playability background."},{"cited_title":"https://github.com/tcsprojects/pgsolver","cited_arxiv_id":null,"evidence_quote":"It provides the parity-game solver used by the game-based model checking variants."},{"cited_title":"In: Verification, Model Checking, and Abstract Interpretation, VMCAI 2024","cited_arxiv_id":null,"evidence_quote":"It describes the generic model-checking environment in which both semantics are implemented."}],"review_version":1}