{"id":"0de5403e-4084-4efa-a749-78e4ecdc8f6a","arxiv_id":"2411.17250","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Weakly acyclic diagrams generalize OBDDs to infinite weakly acyclic languages while retaining top-down memoized algorithms and canonical representations.","lead":"Researchers introduce weakly acyclic diagrams, a data structure that extends ordered binary decision diagrams from finite bit strings to certain infinite regular languages. The extension gives a generic symbolic verifier competitive with specialized tools on lossy channel systems, Petri nets, and broadcast protocols.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Broadcast-protocol section omits the WSTS order/monotonicity proof; the claim that backward reachability applies to this class is therefore not yet discharged.","rationale":"The core WAD contribution—canonical node tables, memoized complement/intersection/union (Algorithms 2–3), and the two Pre procedures (Algorithms 4–5)—is internally consistent, and the appendix proofs for canonicity and cycle contraction check out. I did not find a correctness flaw in the central data-structure claim. The weakest point is the transfer to one of the advertised application classes: broadcast protocols. Section 5's generic argument that Pre_Tt(enc(X)) is weakly acyclic requires a monotone well-quasi-order and explicit upward-closure encodings; these are supplied for lossy channel systems and Petri nets but not for broadcast protocols. The paper's own Section 6 limitation about 7 'unknown' regular-model-checking instances is openly disclosed and lies outside the WSTS guarantees, so I do not treat it as load-bearing for the central claim. My proposed analytical check would settle whether the broadcast gap is only a missing standard proof or a genuine obstruction; if the subword order works as expected, the CONDITIONAL verdict remains appropriate without further changes.","tokens_in":22651,"tokens_out":20369,"duration_ms":201160,"concrete_test":"Add to Section 5.3 an explicit definition of the partial order as the scattered subword order on P*, and prove for each transition type (local, b!/b?, c!!/c??) that the transducer of Figure 6 realizes exactly the one-step relation and that this relation is monotone. Then give the weakly acyclic expression for enc(↑C), e.g., Σ* c1 Σ* ... cm Σ* for C = c1...cm. As a sanity check, exhaustively enumerate all pairs (C,D) with |C|,|D| ≤ 4 for the Figure 6 protocol and verify that D ∈ Pre_Tt(enc(↑C)) iff D ∈ enc(↑Pre(C)); if this passes, the gap is a presentation issue rather than a correctness flaw.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 5's generic argument that Pre_Tt(enc(X)) is necessarily weakly acyclic depends on each modeled class having (i) a monotone transition relation with respect to a well-quasi-order and (ii) weakly acyclic encodings of upward-closed sets. This is explicitly discharged for lossy channel systems (Section 5.1) and Petri nets (Section 5.2), but Section 5.3 introduces broadcast protocols, gives transducers, and asserts applicability without ever defining the partial order on configurations or proving monotonicity of local, rendez-vous, and broadcast transitions. The broadcast step is global ('any other process that can take c?? takes it'), so monotonicity is not immediate from the local transducer picture. Consequently, the statement 'since Pre(X) is upward-closed by monotonicity, Pre_Tt(enc(X)) is necessarily weakly acyclic' has no established instance for broadcast protocols, and the 32/38 empirical solves on this class cannot be interpreted as soundness evidence until the missing order and proof are supplied. This is an omission, not an observed contradiction; likely the standard scattered subword order repairs it.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces weakly acyclic diagrams (WADs), a canonical data structure for weakly acyclic languages, i.e., languages accepted by DFAs whose only cycles are self-loops. It recasts OBDDs as minimal DFAs for fixed-length languages and generalizes them to possibly infinite weakly acyclic languages. The core contributions are: (i) the master-automaton construction, giving a unique minimal WAD per language; (ii) a node-table implementation with a make procedure that maintains canonicity; (iii) OBDD-style top-down algorithms for complement, intersection, and fixed-length Pre/Post with complexity bounds; and (iv) an application to backward reachability for lossy channel systems, Petri nets, and broadcast protocols, implemented in the wadl prototype and evaluated on more than 200 instances.","tokens_in":90,"tokens_out":9003,"duration_ms":245451,"significance":"If correct, WADs are a valuable addition to symbolic verification: they extend the algorithmic advantages of OBDDs to an infinite class of languages while retaining canonical minimal representations. The theoretical development is self-contained, the main correctness proofs are supplied in the appendix, and the artifact is available. The experiments, especially on lossy channel systems and Petri nets, support the claim that the generic approach is competitive with dedicated tools. The main weakness is the broadcast-protocol section, which omits the well-structured transition system order and monotonicity proof and leaves the transducer encoding of the global broadcast step informal; until those are supplied, the applicability to broadcast protocols is not fully established.","major_comments":[{"comment":"The broadcast-protocol section never defines a partial order on configurations nor proves monotonicity of the transition relation. The general recipe in Section 5 relies on the assertion that 'since Pre(X) is upward-closed by monotonicity, Pre_{T_t}(enc(X)) is necessarily weakly acyclic'; for broadcast protocols this inference is not discharged. This is load-bearing because Algorithm 4's correctness (Proposition 10) assumes that the language being transformed is weakly acyclic, so the 32/38 empirical solves cannot be interpreted as soundness evidence until the missing order and monotonicity proof are supplied. Please define the order (e.g., the scattered subword order on state words), prove monotonicity for local, rendez-vous, and broadcast transitions, specify enc(↑C) for this class, and clarify whether the number of processes m is fixed or a parameter.","section":"Section 5.3 / Section 5 general recipe"},{"comment":"The transducer encoding for broadcast is underspecified. Broadcast has a global synchronization step ('any other process that can take c?? takes it'), while the operational semantics is given as a length-preserving transducer on words. The paper should specify how a one-pass letter-to-letter transducer guesses the sender and handles receivers that occur before the sender in the word, and it should prove that the transducer's relation coincides with the broadcast transition relation. Without this, it is not clear that Algorithm 4 is being applied to the correct relation.","section":"Section 5.3 / Figure 6"},{"comment":"The pre-compatibility tweak 'slightly changes the semantics' of read transitions, and the authors justify it by saying that processes in a common state are indistinguishable and in the benchmarks never share states. This is an unproven, benchmark-specific assumption; the reported comparison with BML and McScM is therefore not strictly a comparison on the original lossy-channel semantics. Please either prove the equivalence for the class of systems considered or clearly state that the comparison is for a restricted-read variant.","section":"Section 6, lossy channel systems experiments"}],"minor_comments":[{"comment":"There is a typo in 'minimial DFA' in the paragraph after Figure 1.","section":"Section 2"},{"comment":"The phrase 'exponential worse-case time complexity' should be 'worst-case time complexity'.","section":"Section 4.2"},{"comment":"The notation p_(a,b) assumes a total order on the alphabet Σ×Σ for indexing node successor tuples; please state that order explicitly, since the data structure definition in Section 3 only fixes an order for a one-dimensional alphabet.","section":"Section 4.3 and Section 5.3"},{"comment":"In the monotonicity proof for read transitions, the phrase 'converts w′_i into avy′' appears to be a typo for the suffix after the first a, which is v a y′; as written the notation is confusing.","section":"Appendix E, Proposition 12 proof"}],"recommendation":"major_revision","confidential_remarks":"The paper is a strong candidate after revision. The main gap, the missing well-quasi-order and monotonicity proof for broadcast protocols, is likely fixable with a standard subword order argument. I would support acceptance if the authors add the missing definitions and proofs and adjust the lossy-channel experimental claims to acknowledge the restricted-read tweak."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague, here's my read. The paper delivers on its central claim: it gives a data structure for weakly acyclic languages—the class already known as R-trivial or partially ordered—that carries over the OBDD toolbox. The node table representation is simple, canonical, and the memoized top-down algorithms for complement and intersection transfer with the same complexity bounds. The core proofs (Propositions 1–10) are written out and look correct; the master automaton is a definitional device, not a circular crutch. The authors are upfront that the languages themselves were studied before, and they position the novelty as the data structure and the verification pipeline. That is honest and accurate. The benchmarking is also more credible than most. They compare against dedicated tools (BML, McScM, mist), report timeouts and unknowns, and ship an artifact. On LCS and Petri nets the results are genuinely competitive. That's real evidence of utility, not just a toy. Where it gets soft is Section 5.3. For LCS and Petri nets they define the partial order and show monotonicity. For broadcast protocols they give transducers and declare the backward reachability framework applies, but never define the order on configurations or prove that local, rendez-vous, and broadcast transitions are monotone. The broadcast step is global and synchronizing, so monotonicity is not automatic from the local transducer picture. The generic claim 'Pre_Tt(enc(X)) is necessarily weakly acyclic' therefore has no established instance for this class. The stress-test note is right. I expect the standard scattered subword order repairs it—the dodo tool already uses encodings of upward-closed sets for these protocols—but as written the section is an assertion, not a proof. This is an omission in the application layer, not a flaw in the core data structure. A second, minor soft spot: Algorithm 4 needs the result to be weakly acyclic as an explicit guarantee, and the regular-model-checking experiments honestly list 7 instances where cycle contraction makes the outcome unknown. That's the authors being straight with the reader, and I count it as a point in their favor. Bottom line: the theoretical core is sound, the empirical claims are measured, and the one real gap is a missing monotonicity proof that is likely a one-paragraph fix. This deserves competent peer review and, after the broadcast order is supplied, publication. I'd bring it to the reading group and I'd cite it if I worked on symbolic infinite-state verification.","headline":"WADs are a clean, honest extension of OBDDs to infinite weakly acyclic languages; the main caveat is an unproved monotonicity claim in the broadcast-protocol section.","tokens_in":23382,"tokens_out":2149,"would_cite":true,"duration_ms":19240,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper introduces weakly acyclic diagrams, a generalization of OBDDs that represents infinite languages canonically while preserving the memoized dynamic-programming algorithms used in symbolic verification.","keywords":["weakly acyclic diagrams","weakly acyclic languages","ordered binary decision diagrams","symbolic model checking","infinite-state verification","well-structured transition systems","backward reachability","regular model checking"],"falsifier":"A decisive test is to apply the contraction-based pre/post algorithm to a fixed-length transducer and a weakly acyclic language whose true pre-image or post-image is known not to be weakly acyclic, such as the paper's own Figure 3 example where the result is $(a+b)^*b$. If the algorithm terminates and returns a WAD whose language differs from the exactly computed pre-image, the claimed correctness guarantee fails; on small alphabets the exact pre-image can be obtained by an independent subset construction.","tokens_in":22334,"feed_emoji":"🔁","tokens_out":7355,"duration_ms":66860,"temperature":0.7,"pith_summary":"Ordered binary decision diagrams (OBDDs) represent Boolean functions as canonical decision graphs, but only for inputs of a fixed length. This paper introduces weakly acyclic diagrams (WADs), which replace fixed length with a weaker restriction: the underlying directed graph may contain only self-loops as cycles. WADs are canonical minimal deterministic automata for weakly acyclic languages, so they can represent infinite regular languages while still supporting the memoized top-down algorithms that make OBDDs fast. Using WADs, the authors implement symbolic backwards reachability for infinite-state systems whose configuration sets are upward-closed and weakly acyclic, including lossy channel systems, Petri nets, and broadcast protocols, and they report that their prototype is competitive with dedicated tools on a broad benchmark suite.","feed_headline":"WADs bring OBDD-style speed to infinite-state verification","feed_subtitle":"Generalizes OBDDs to infinite regular languages, keeping memoized algorithms and enabling backward reachability.","key_machinery":"The load-bearing object is the master automaton over an alphabet $\\Sigma$: its states are all weakly acyclic languages, and reading a letter maps a language to its residual. Because weakly acyclic languages have no infinite descending chains of residuals, every WAD is a finite fragment of this automaton, and that fragment is exactly the minimal DFA for each represented language. The node table representation adds a special self pointer for the case where a residual equals the language itself; memoized recursion over residuals, plus the make procedure that collapses duplicate languages, is what carries all operations.","core_discovery":"The paper's central discovery is that the algorithmic advantages of OBDDs survive when fixed-length Boolean functions are replaced by weakly acyclic regular languages, meaning languages whose minimal DFA has no cycles except self-loops. For such a language, the set of residuals is partially ordered by the transition relation and has no infinite descending chains, so the 'master automaton' whose states are all weakly acyclic languages gives a canonical minimal DFA for each one. A WAD stores finitely many such languages as a shared node table in which a transition may point to a node or to 'self', and a memoized make procedure guarantees that equal languages share one node. Complement, intersection, union, and pre/post along fixed-length relations are then computed by recursive descent through residuals, exactly in the style of OBDD algorithms; in the pre-compatible case the pre-image computation runs in polynomial time, and in general it terminates and returns a correct WAD whenever the result is weakly acyclic.","pith_inferences":["If weakly acyclic languages turn out to be as common in regular model checking benchmarks as the paper's experiments suggest, a unified WAD-based engine could replace several specialized symbolic backends; this is an extrapolation beyond the paper's own claims.","The seven regular-model-checking instances where cycle contraction fires leave the weak acyclicity of the result unproven; a natural next step, not taken here, is to make that contraction step produce a certificate or fall back to exact determinization.","The class could be widened by allowing bounded nondeterminism, following the paper's closing question about languages like $(a+b)^*b$; if such an extension kept canonical residuals it would cover more protocols.","A stress test on parameterized families, such as the ring instances the paper reports scaling to large sizes, could reveal where the residual hierarchy grows too large and where an extrapolation-based widening would be needed."],"forward_implications":["Every weakly acyclic language has a unique minimal WAD representation, generalizing the canonicity of OBDDs to infinite languages.","The standard OBDD operations—negation, conjunction, union, and relational pre/post—can be ported to infinite-state symbolic verification with the same memoization-based complexity guarantees.","Backwards reachability for well-structured transition systems becomes a uniform WAD computation for lossy channel systems, Petri nets, and broadcast protocols, rather than requiring a purpose-built data structure for each system class.","For regular model checking, any run that terminates with all cycle contractions being true self-loops yields a correct answer, and many textbook protocols are weakly acyclic.","Pre-compatibility provides a polynomial-time pre-image computation for many lossy-channel-system encodings, making the infinite-state case tractable in practice."],"supporting_citations":[{"why":"Introduces OBDDs as canonical representations of Boolean functions, the fixed-length setting that WADs generalize.","marker":"[8,13]"},{"why":"Presents OBDDs as minimal DFAs for fixed-length languages and the memoized dynamic-programming algorithms WADs adapt.","marker":"[20]"},{"why":"Establishes backward reachability for well-structured transition systems and the upward-closed fixpoint theorem that WAD verification builds on.","marker":"[23,3]"},{"why":"Introduces lossy channel systems and their verification, one of the three main application classes.","marker":"[4,6]"},{"why":"Defines Petri nets, the second main application class.","marker":"[31]"},{"why":"Defines broadcast protocols, the third main application class.","marker":"[21]"},{"why":"Supplies the dedicated interval and covering-tree data structures for upward-closed sets against which the WAD implementation is compared.","marker":"[18,24]"},{"why":"Provide the lossy-channel-system benchmark tools and instances used in the experiments.","marker":"[25,26,27]"}],"fun_headline_variants":["WADs: OBDD-style speed for infinite-state verification","Infinite-state checking gets OBDD-efficient algorithms","Weakly acyclic diagrams: OBDDs for infinite languages","Extending OBDD power to infinite-state verification"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The framework depends on the chosen encoding mapping every upward-closed set that the backward reachability algorithm ever constructs to a weakly acyclic language, and on each transition's transducer preserving weak acyclicity under pre-image.","fun_headline_variants_meta":{"raw":{"variants":["WADs: OBDD-style speed for infinite-state verification","Infinite-state checking gets OBDD-efficient algorithms","Weakly acyclic diagrams: OBDDs for infinite languages","Extending OBDD power to infinite-state verification"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000173,"raw_usage":{"total_tokens":1228,"prompt_tokens":847,"completion_tokens":381,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":463,"completion_tokens_details":{"reasoning_tokens":313}},"tokens_in":463,"tokens_out":381,"duration_ms":4029,"temperature":1.0,"reasoning_tokens":313,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T12:20:49.558237+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A decisive test is to apply the contraction-based pre/post algorithm to a fixed-length transducer and a weakly acyclic language whose true pre-image or post-image is known not to be weakly acyclic, such as the paper's own Figure 3 example where the result is $(a+b)^*b$. If the algorithm terminates and returns a WAD whose language differs from the exactly computed pre-image, the claimed correctness guarantee fails; on small alphabets the exact pre-image can be obtained by an independent subset construction.","supporting_citations":[{"cited_title":"MIT Press (2023)","cited_arxiv_id":null,"evidence_quote":"Presents OBDDs as minimal DFAs for fixed-length languages and the memoized dynamic-programming algorithms WADs adapt."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Defines broadcast protocols, the third main application class."}],"review_version":1}