{"id":"79258379-ccd4-4f4e-98d7-3807a0d0f0be","arxiv_id":"2411.13412","paper_version":3,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A categorical generalization of the W-method yields provably complete conformance test suites for DFAs, Mealy and Moore machines, and new instances for weighted and nominal automata.","lead":"This paper develops a category-theoretic framework for proving that test suites completely certify equivalence between a specification automaton and a black-box implementation. It generalizes the classical W-method to a wide class of automata, including the first complete test suites for weighted and nominal automata.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The W-method generalization is complete only for fault domains that already assume a state cover on the implementation; classical m-completeness via Lemma 2.5 is not recovered, so the main results are conditional, not full m-complete test suites.","rationale":"The proof of Theorem 4.9 appears sound: the AM-bisimulation argument is standard, and the use of minimality and characterization morphisms in Lemma C.8 is legitimate. I found no mathematical error in the central derivation. The weakest assumption identified by the reader (preservation of countable coproducts by X⊗−) is indeed necessary for constructing the word object and the initial algebra, but it holds in all categories used in the applications (Set, Vect_K, Nom, Pos), so it does not threaten the intended scope. The more serious issue is the gap between the claimed generalization of the W-method and the actual fault domains. The classical W-method gives m-completeness: a test suite that is complete for every implementation with at most m states, where m = n+k. The categorical result is complete only for implementations that already satisfy a state-cover condition tied to the chosen p and k. The authors are transparent about not proving Lemma 2.5, but the abstract and Section 5.1 still say they 'recover the W-method' for DFAs, Moore machines and Mealy machines. Because of this, a reader could easily overestimate the power of the result. This concern is load-bearing for the contribution's significance: if the state-cover assumption is not derivable from an implementation bound, the framework provides a conditional completeness theorem rather than a full generalization of the W-method. The concrete test would settle the matter by checking whether the DFA instance plus the categorical machinery is sufficient to recover the classical m-completeness. If it is not, the paper should be revised to qualify the claims.","tokens_in":39441,"tokens_out":24195,"duration_ms":234871,"concrete_test":"Instantiate the framework in the DFA case and attempt to prove, using only the categorical tools of Sections 3–4, that every DFA M with at most n+k states satisfying S∼_{P·W}M belongs to U^k_p (a categorical analogue of Lemma 2.5). If such a proof cannot be given without introducing a separate size-based argument, the paper's claim to recover the W-method is only partial; the abstract and Section 5.1 should then be revised to state explicitly that the test suites are complete only w.r.t. the state-cover fault domains, not w.r.t. state-count bounds.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central completeness result, Corollary 4.13, states that t^k_{p,w} is complete for S with respect to U^k_p = {M | (p·j_k, δ_C) is a weak state cover for M}. This fault domain is defined by a structural reachability assumption on the implementation, not by a bound on its size. The paper explicitly does not generalize the classical Lemma 2.5, which derives exactly this state-cover property for any implementation with at most n+k states from agreement on P·W. Consequently, the framework does not imply the classical n+k-completeness of the W-method: from Corollary 4.13 one cannot conclude that T^k_{P,W} is complete for all DFAs with at most n+k states, unless one separately proves the DFA-specific Lemma 2.5. In Section 5.1 the authors state they 'recover the W-method' for DFAs, Moore and Mealy machines, but only Lemma 2.6 is recovered. For weighted and nominal automata, the fault domains U^k_P are likewise defined by the state-cover condition, so the 'complete test suites' are conditional on a property of the black-box implementation that is not established from any implementation bound. This is not an error in the proof, but it is a significant gap between the paper's framing as a generalization of the W-method and what is actually shown.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a categorical framework for conformance testing of automata in monoidal closed categories. It defines generalized test suites, fault domains, weak state covers, and characterization morphisms, and proves a categorical completeness theorem (Theorem 4.9, Corollary 4.13): if a minimal specification S and an implementation M agree on the generalized W-test suite t^k_{p,w}, and M belongs to the fault domain U^k_p consisting of automata for which p·j_k is a weak state cover, then S and M are language-equivalent. The framework is instantiated to recover test-suite completeness for DFAs, Moore machines, and Mealy machines, and to derive new completeness results for weighted automata and deterministic nominal automata. The proofs are deferred to detailed appendices, with a categorification of the AM-bisimulation proof of the classical Lemma 2.6.","tokens_in":39704,"tokens_out":13758,"duration_ms":154588,"significance":"If the results are correct, the paper provides a valuable unification of W-method-style completeness proofs at a high level of abstraction, and it gives the first completeness results for weighted and nominal automata in this testing setting. The appendices contain extensive proofs, and the examples are worked in enough detail to be checkable. The main caveat is that the completeness results are relative to fault domains defined by a state-cover condition on the implementation, not by a bound on the number of states; classical m-completeness is therefore not recovered at the general level. This conditional nature should be reflected in the paper's claims, but it does not invalidate the technical content.","major_comments":[{"comment":"The paper's framing overstates what is proved. Corollary 4.13 establishes completeness of t^k_{p,w} only with respect to U^k_p = {M | (p·j_k, δ_C) is a weak state cover for M}. For DFAs, Moore machines, and Mealy machines, the classical W-method's n+k-completeness (Corollary 2.7) additionally requires Lemma 2.5, which derives the state-cover property for any implementation with at most n+k states from agreement on P·W. The paper explicitly does not generalize Lemma 2.5, and consequently the abstract and Section 5.1 claims of 'recovering the W-method' are too strong: what is recovered is the test-suite construction and the completeness argument of Lemma 2.6, not the full m-complete fault-domain result. This is a load-bearing scope issue for the central claim, and it should be corrected either by adding an explicit statement that m-completeness is not derived, or by proving a categorical analogue of Lemma 2.5 for the concrete instances.","section":"Corollary 4.13, Section 5.1, Section 5.2, Section 5.3"}],"minor_comments":[{"comment":"In the proof of Proposition 5.4(ii), the string 'LS.[s2]|W' should read 'LS(s2)|W'.","section":"Appendix D.4"},{"comment":"There is a typo in 'classes of of automata'; the duplicated 'of' should be removed.","section":"Section 2"},{"comment":"The PDF title contains an extra space in 'Complete T est Suites'; this should be fixed in the camera-ready version.","section":"Title"},{"comment":"In the nominal automata example, the sentence 'Hence, we obtain the complete test suite T^0_{P,W}' should explicitly recall that completeness is with respect to the fault domain U^0_p defined in Theorem 5.9, so that the conditional nature of the result is not lost in the example.","section":"Section 5.3"}],"recommendation":"major_revision","confidential_remarks":"The technical content appears sound; my concern is not with the proofs but with the gap between the abstract's claim of recovering the W-method and the actual conditional completeness results. If the authors revise the framing to state clearly that m-completeness is not recovered and that all instances are complete only with respect to state-cover fault domains, I would be willing to accept the paper."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Kocsis and Rot have a real result here: a categorical version of the W-method's completeness lemma, with the first test suites for weighted and nominal automata. The main theorem (4.9) and its corollary (4.13) are proved in detail by categorifying the AM-bisimulation argument from Kruger et al., and the applications are worked out carefully. The framework is clean: weak state covers and characterization morphisms really do capture the relevant structure, and the recovery of the classical DFA case checks out.\n\nThe soft spot is the one the stress-test put its finger on. Corollary 4.13 is complete for the fault domain U^k_p, which is defined by the assumption that p·j_k is a weak state cover of the implementation. That is a reachability condition on the black-box system, not a bound on its size. The paper states plainly that it does not generalize Lemma 2.5, so the classical n+k-completeness of the W-method is not derived from the categorical machinery. For DFAs, Moore and Mealy machines, the old lemma does the job and you get m-completeness as before. For weighted and nominal automata, the new 'complete test suites' are complete only for implementations that already satisfy the state-cover property. That is a genuine limitation, and the paper's phrasing—'recover the W-method'—is a bit generous, but the authors are transparent about it in the introduction and in the fault-domain definitions. It is not a hidden circularity; it is a scope issue.\n\nThere are also minor issues: a typo in the proof of Proposition D.4 ('LS.[s2]|W'), and the novelty claim about first test suites for weighted/nominal automata would benefit from a careful comparison with Moerman's thesis, which the reader flagged. Neither affects the main theorem.\n\nThe tensor-preservation assumption (X ⊗ − preserves countable coproducts) is reasonable for the intended categories: Set, Vect_K, Nom. No problem there.\n\nWho is this for? Anyone working on categorical automata learning or conformance testing for weighted and nominal systems. The paper deserves a serious referee; the proofs are extensive and the framework is worth engaging with. I would accept it with a request to clarify the fault-domain framing and to make the DFA recovery of m-completeness explicit.","headline":"A genuinely categorical W-method completeness lemma with new weighted/nominal test suites, but completeness is relative to reachability-condition fault domains, not size bounds.","tokens_in":40235,"tokens_out":3147,"would_cite":true,"duration_ms":31463,"reading_group":"yes","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 proves that the classical W-method for conformance testing works for every automaton living in a monoidal closed category, provided the specification is minimal and supplied with a state cover and a characterization morphism.","keywords":["conformance testing","complete test suites","W-method","monoidal closed categories","coalgebra","automata learning","weighted automata","nominal automata"],"falsifier":"Take the weighted automaton S of Section 5.2 with P={ε,b}, W={ε,b}, k=1, and solve the linear equations LS|T = LM|T for a five-state implementation M whose P·$Σ^{{≤1}}$ spans its state space. If any solution has LS≠LM, the suite is not complete and Theorem 5.7 falls; the paper reports its faulty example is rejected, so the expected outcome is that no such solution exists.","tokens_in":39226,"feed_emoji":"🧪","tokens_out":7845,"duration_ms":80977,"temperature":0.7,"pith_summary":"This paper claims that the classical W-method for conformance testing works not just for finite automata but for any automaton that lives in a monoidal closed category — a setting in which machines can be seen simultaneously as algebras and as coalgebras. The method needs two ingredients: a state cover, a set of words that reaches every state of the specification, and a characterization set, a set of words that separates any two semantically different states. Given those, the paper's main theorem produces a test suite that is complete with respect to implementations with bounded reachability: any implementation in the fault domain that passes all tests is genuinely equivalent to the specification. The theorem recovers the known W-method for deterministic finite automata, Moore machines, and Mealy machines, and it yields, to the paper's knowledge, the first complete test suites for weighted automata and for deterministic nominal automata. The practical point is that equivalence queries in automata learning, often the bottleneck, can be discharged by test suites in a much wider class of models.","feed_headline":"Complete test suites for any automaton in a monoidal closed category","feed_subtitle":"Recovers the W-method for DFA, Moore, and Mealy machines; adds first complete suites for weighted and nominal automata.","key_machinery":"The machinery is the dual view of an automaton $(Q,i_Q,\\delta_Q,f_Q)$ as an $F$-algebra for $FX=I+X\\otimes\\Sigma$ and a $G$-coalgebra for $GX=O\\times[X,\\Sigma]$. Words $\\Sigma^*$ are the initial $F$-algebra, and languages $[\\Sigma^*,O]$ are the final $G$-coalgebra, so the reachability map $r_A:\\Sigma^*\\to Q$ and the language map $l_A:Q\\to[\\Sigma^*,O]$ are uniquely determined. A state cover $p:P\\to\\Sigma^*$ is a map containing the empty word such that $r_S\\circ p$ is a split epimorphism; a weak state cover additionally carries a transition map $\\delta_C$ that follows the transitions of $S$ on the covered words. A characterization morphism $w:W\\to\\Sigma^*$ is a map such that equality of languages restricted to $W$ implies equality of full languages for every parallel pair of states. The generalized W-method composes these as $t^k_{p,w}=p\\cdot j_{k+1}\\cdot w$, where $j_{k+1}$ is the inclusion of words of length at most $k+1$; completeness is shown by turning test agreement into an AM-bisimulation, a categorical bisimulation connecting the two automata, and finality of the language coalgebra then forces language equivalence.","core_discovery":"The load-bearing result is Corollary 4.13: for any minimal automaton $S$ in a monoidal closed category, any morphism $p: P \\to \\Sigma^*$, any characterization morphism $w: W \\to \\Sigma^*$ for $S$, and any $k \\in \\mathbb{N}$, the generalized W test suite $t^k_{p,w} = p \\cdot j_{k+1} \\cdot w$ is complete for $S$ with respect to the fault domain $U^k_p = \\{M \\mid (p \\cdot j_k, \\delta) \\text{ is a weak state cover for } M\\}$. In words: if an implementation $M$ in this fault domain agrees with $S$ on all test words, then $M$ and $S$ recognize the same language. The proof shows that agreement on the test suite lets one construct a categorical bisimulation between the reachable parts of $S$ and $M$, so equivalence follows from finality of the language coalgebra.","pith_inferences":["The same theorem probably extends to weighted automata over semirings, since the paper's machinery only needs the category of semimodules to preserve countable coproducts; this is not shown in the paper and would require new state-cover and characterization-set algorithms.","The weak-state-cover notion was motivated by ordered automata, where ordinary state covers cannot exist; a reader might expect complete test suites for ordered automata to follow from Corollary 4.11 even though the paper does not spell out that instance.","The paper stops at completeness and does not say how to compute state covers and characterization sets for weighted or nominal automata; without such algorithms, the new complete suites are existential guarantees rather than directly usable test generators."],"forward_implications":["For deterministic finite automata, Moore machines, and Mealy machines, the generalized theorem reproduces the standard W-method and its completeness, so one proof covers all three.","For weighted automata over a field, Theorem 5.7 gives a complete test suite: implementations in $U^k_P$ that agree on $P\\cdot\\Sigma^{\\le k+1}\\cdot W$ must have identical weighted languages.","For deterministic nominal automata, Theorem 5.9 gives a complete test suite; the paper's worked example is infinite but orbit-finite, hence finitely presentable in the nominal sense.","Because completeness is unchanged under factorization (Corollary 4.16), the abstract morphism-based test suite can be replaced by its image, matching the subset-based notion used in practice."],"supporting_citations":[{"why":"Chow's W-method: the classical m-complete test suite construction this paper generalizes.","marker":"[21]"},{"why":"Vasilevskii's W-method: original completeness theorem for finite automata that Corollary 2.7 rederives.","marker":"[54]"},{"why":"Supplies the bisimulation-based proof that the categorical Theorem 4.9 categorifies.","marker":"[35]"},{"why":"Goguen's machines in monoidal closed categories, source of the word-object initial algebra.","marker":"[26]"},{"why":"Arbib and Manes on adjoint machines and the duality between reachability and observability used for state covers and characterization morphisms.","marker":"[6]"},{"why":"Urbat and Schröder's categorical automata learning framework, source of the final-coalgebra view of languages.","marker":"[51]"},{"why":"Weighted automata as the model instantiated in Section 5.2.","marker":"[24]"},{"why":"Nominal automata as the model instantiated in Section 5.3.","marker":"[11]"}],"fun_headline_variants":["Generalized W-method for all automata in monoidal closed categories","Categorical test suites: complete for weighted and nominal automata","W-method generalized to monoidal closed categories","Complete test suites for any automaton, categorically","Generalizing the W-method to categorical automata"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole construction assumes that for every object X the functor $X\\otimes -$ preserves countable coproducts; if some category of interest fails that, the word object, concatenation, state covers, and the W test suite cannot even be formed.","fun_headline_variants_meta":{"raw":{"variants":["Generalized W-method for all automata in monoidal closed categories","Categorical test suites: complete for weighted and nominal automata","W-method generalized to monoidal closed categories","Complete test suites for any automaton, categorically","Generalizing the W-method to categorical automata"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000829,"raw_usage":{"total_tokens":3589,"prompt_tokens":878,"completion_tokens":2711,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":494,"completion_tokens_details":{"reasoning_tokens":2630}},"tokens_in":494,"tokens_out":2711,"duration_ms":19854,"temperature":1.0,"reasoning_tokens":2630,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:26:08.799768+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the weighted automaton S of Section 5.2 with P={ε,b}, W={ε,b}, k=1, and solve the linear equations LS|T = LM|T for a five-state implementation M whose P·$Σ^{{≤1}}$ spans its state space. If any solution has LS≠LM, the suite is not complete and Theorem 5.7 falls; the paper reports its faulty example is rejected, so the expected outcome is that no such solution exists.","supporting_citations":[{"cited_title":"IEEE Trans","cited_arxiv_id":null,"evidence_quote":"Chow's W-method: the classical m-complete test suite construction this paper generalizes."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Vasilevskii's W-method: original completeness theorem for finite automata that Corollary 2.7 rederives."},{"cited_title":"In: TACAS (2)","cited_arxiv_id":null,"evidence_quote":"Supplies the bisimulation-based proof that the categorical Theorem 4.9 categorifies."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Goguen's machines in monoidal closed categories, source of the word-object initial algebra."},{"cited_title":"Journal of Pure and Applied Algebra 6(3), 313–344 (1975)","cited_arxiv_id":null,"evidence_quote":"Arbib and Manes on adjoint machines and the duality between reachability and observability used for state covers and characterization morphisms."},{"cited_title":"In: LICS","cited_arxiv_id":null,"evidence_quote":"Urbat and Schröder's categorical automata learning framework, source of the final-coalgebra view of languages."},{"cited_title":"In: Handbook o f Automata Theory (I.), pp","cited_arxiv_id":null,"evidence_quote":"Weighted automata as the model instantiated in Section 5.2."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Nominal automata as the model instantiated in Section 5.3."}],"review_version":1}