{"id":"a89927b1-a630-47bf-b7aa-958ac122c9f5","arxiv_id":"1909.01627","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For k-synchronizable communicating automata, reachability checking and deciding whether a system is k-synchronizable are both decidable, with corrected mailbox proofs and new peer-to-peer results.","lead":"This paper fixes flawed proofs about k-synchronizable message-passing systems, where every execution can be reordered into short send-receive phases. It shows that reachability checking and deciding k-synchronizability are both possible, for mailbox and peer-to-peer communication models.","discovery_kind":"first_principles","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Fig. 4's update clause for C_R sets is vacuous for X=R, so the abstraction underpinning Lemma 1 cannot compute the receivers needed for causal delivery as printed.","rationale":"The paper's central claim is that reachability and k-synchronizability are decidable, with the proofs flowing through the finite abstraction of Fig. 4 and Lemma 1. The reader correctly identified the Section 4 abstraction as the weakest assumption. My stress-test found a concrete defect in that abstraction as printed: the update clause for C_R sets cannot fire when X=R, so the abstraction fails to record exactly the receivers that Lemma 1's invariant requires. This is not a mere disagreement with a proof style; it is an internal inconsistency with the paper's own Example 4. The paper otherwise gives a coherent picture: it identifies real flaws in [4], provides counterexamples, and the overall structure of the finite-state construction is plausible. Because the defect may be a simple typo (v∩X instead of v′∩X) rather than a conceptual impossibility, I recommend a conditional verdict: the paper should be accepted only after the rule is corrected and Lemma 1's induction is re-verified against the corrected rule. If the correction fails to restore the invariant, the reachability decidability proof collapses; if it succeeds, the central claims likely stand.","tokens_in":34479,"tokens_out":12988,"duration_ms":130322,"concrete_test":"Recompute Example 4 using exactly the formula in Fig. 4: build the local conflict graph of e1, set Unmp = {v1, ψ_r}, and check whether any pair (v, v′) with v ∈ Unmp, v SS /-> v′, and v ∩ R ≠ ∅ exists. The set is empty, so C′_{R,r} remains ∅, contradicting the displayed {s} and the invariant used in Lemma 1. Then change the guard to v′ ∩ X ≠ ∅, re-run the same computation, and independently verify that the corrected rule maintains the claimed invariant of Lemma 1 through the full induction, including dependencies propagated across three or more k-exchanges.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The decidability of reachability (Theorem 3) rests on Lemma 1, which in turn rests on the transition relation of Fig. 4. In the last component of the definition of C′_{X,p}, Fig. 4 contains the clause {procX(v′) | v SS /-> v′, v ∈ Unmp, v ∩ X ≠ ∅}. For X=R this clause is empty: every v ∈ Unmp is an unmatched send, or the summary node ψ_p that abstracts unmatched sends, so v ∩ R = ∅. Yet C_R,p exists precisely to record receivers of messages sent causally after an unmatched message, i.e. values procR(v′) for targets v′ with v′ ∩ R ≠ ∅. The paper's own Example 4 exposes the failure: after e1 = send(q,r,v1)·send(q,s,v2)·rec(q,s,v2), the edge v1 SS /-> v2 should contribute C′_{R,r} = {s}; with the printed guard, v1 ∩ R = ∅ so the clause contributes nothing and C′_{R,r} stays ∅. If this is a typo and the guard should be v′ ∩ X ≠ ∅, the example and the intended invariant are restored, but the manuscript as written gives an inconsistent transition relation, and the proof of Theorem 3 is not sound in its printed form.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies k-synchronizability for communicating automata with mailbox and peer-to-peer semantics. It gives a graph-theoretic characterization of k-synchronous MSCs and of causal delivery, then builds finite-state abstract transition relations to show that reachability is decidable for k-synchronizable systems (Theorems 3 and 5) and that k-synchronizability itself is decidable (Theorems 4 and 6), while repairing flaws in the earlier work [4]. The main technical device is a summary-node abstraction (the nodes ψ_p) that carries the inter-k-exchange information needed to detect causal-delivery violations, together with instrumented-system constructions for the membership problem.","tokens_in":34752,"tokens_out":8298,"duration_ms":86457,"significance":"If the constructions are correct, the paper makes a substantial contribution: it identifies concrete errors in [4] (Example 2 for the SCC/Hamiltonian-cycle issue, Fig. 5 for causal delivery, Example 8 for the feasibility monitor), provides self-contained proofs in an appendix, extends both decidability results to peer-to-peer systems, and states crisp graph-theoretic characterizations (Theorems 1 and 2). The claimed decidability results are the kind of foundational facts that the verification community needs to be able to rely on, so the paper is worth publishing once the technical issues below are resolved.","major_comments":[{"comment":"The last union term in the definition of C′_{X,p} reads {procX(v′) | v SS -> v′, v ∈ Unmp, v ∩ X ≠ ∅}. For X = R this clause is vacuous, because every v ∈ Unmp is either an unmatched send or a summary node ψ_p, so v ∩ R is always empty. Yet C_{R,p} is supposed to record the receivers of messages sent causally after an unmatched send, and the paper's own Example 4 and Fig. 5c state that for e1 = send(q,r,v1) · send(q,s,v2) · rec(q,s,v2), the computation yields C′_{R,r} = {s}. With the printed guard, C′_{R,r} remains empty. Since Lemma 1 and hence Theorem 3 (as well as the feasibility construction in §5, which reuses these sets) depend on this transition relation, the printed definition is not sound. The natural fix is to replace the guard v ∩ X ≠ ∅ by v′ ∩ X ≠ ∅, which would restore Example 4 and the intended invariant, but the manuscript must be corrected and the proof of Lemma 1 rechecked under that correction.","section":"§4, Fig. 4"},{"comment":"The inductive invariants stated at the start of the proof of Lemma 1 do not match the definitions of C_{S,p} and C_{R,p} in §4. In the main text, C_{S,p} is defined as {procS(v) | v′ SS -> v, v′ unmatched, procR(v′) = p} and C_{R,p} as {procR(v) | v′ SS -> v, v′ unmatched, procR(v′) = p, v ∩ R ≠ ∅}. In the proof, however, the induction hypothesis is written as C_{S,p} = {procS(v′) | v SS -> v′, v not matched, procS(v) = p} and C_{R,p} = {procR(v′) | v SS -> v′, v not matched, procR(v) = p, v′ ∩ R ≠ ∅}. These are different sets indexed by different processes, so the induction is not anchored to the same invariant as the transition relation in Fig. 4. This discrepancy must be repaired for the proof of Theorem 3 to be sound as written.","section":"§4, proof of Lemma 1"}],"minor_comments":[{"comment":"The condition \"no RS edge occurs on any cyclic path\" is slightly imprecise; the proof in the appendix works with strongly connected components and cycles, so it would be clearer to state the condition as \"no RS edge occurs on any cycle\".","section":"§3, Theorem 1"},{"comment":"The variable p is used both as the index of the set being updated and as a bound variable in the second union term of C′_{X,p} (the term {p | p ∈ C_{X,q}, ...}). This overloading makes the rule hard to read and should be renamed.","section":"§4, Fig. 4"},{"comment":"The examples illustrating feasibility and badness (Fig. 8) are placed in Appendix A rather than in the main text; a forward reference from Definition 9 would help the reader connect the definitions to the counterexamples.","section":"§5, Definition 9"},{"comment":"The arrow symbols in the submitted text appear as garbled tokens such as \"/axisshort/axisshort/arrowaxisright\"; the final version should use proper glyphs for the extended-edge relation.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The main error in Fig. 4 appears to be a localized typo (v ∩ X instead of v′ ∩ X), and the paper is otherwise detailed enough that I expect a fix to be feasible within the scope of a revision. I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe useful core here is real: the authors pin down why Bouajjani et al.'s CAV 2018 proofs for mailbox k-synchronizability do not go through, and they replace them with new machinery. The SCC-based characterization (Theorem 1), the extended conflict graph for causal delivery (Theorem 2), and the summary-node construction for recognizing k-synchronous MSCs are genuinely different from [4], and the counterexamples to the old proofs are concrete and convincing. The appendix carries full proofs of all six theorems, and the prose is careful about where [4] fails. This is a repair paper with enough new content to be worth publishing if the central construction is fixed.\n\nThe soft spot is not a deep conceptual one, but it is load-bearing. As printed, the update rule for C′_{X,p} in Fig. 4 has the condition v ∩ X ≠ ∅ in the last unioned set. For X = R, every v in Unmp is either an unmatched send or a summary node, so it has no receive action in it; the clause contributes nothing. That makes C′_{R,p} unable to record receivers of matched messages sent causally after an unmatched message, which is exactly what C_{R,p} is for. Example 4 in the paper demonstrates the contradiction: the bookkeeping shown for e1 requires C′_{R,r} = {s}, but with the printed guard that set stays empty. The fix is almost certainly to write v′ ∩ X ≠ ∅, which matches the invariant stated just above Fig. 4 and makes Example 4 work. As it stands, though, Lemma 1 and therefore Theorem 3 are not sound in the printed form.\n\nEverything else I checked is in better shape. The counterexamples in the appendix are honest and targeted. The peer-to-peer extension is less surprising but coherent; the simplified causal-delivery check there is plausible and the proofs are analogous. The main residual risk is the same as the reader's: the inductive proofs, especially Lemma 1 and Lemma 4, are dense, and no formalization is provided. Given the typo, I would not trust the artifact without an independent check, but the intended construction appears sound.\n\nWho this is for: anyone working on bounded asynchrony, synchronizability, or regular model checking of communicating automata. If the authors fix Fig. 4 and re-verify the induction, this deserves a serious referee and likely publication. I would send it out with the request that the referee re-check the transition relation and the proof of Lemma 1 line by line.","headline":"A mostly solid repair of known decidability claims for k-synchronizable systems, but one printed typo in the central transition relation (Fig. 4) breaks the proof as written.","tokens_in":35292,"tokens_out":3960,"would_cite":true,"duration_ms":35776,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q85","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Both reachability and k-synchronizability are decidable for k-synchronizable systems.","keywords":["k-synchronizability","communicating automata","mailbox communication","peer-to-peer communication","reachability","decidability","causal delivery","message sequence charts"],"falsifier":"Enumerate all MSCs over a small system, say three processes and three messages with k=2, and compare the language accepted by the abstract transition relation $\\overset{e,k}{\\Longrightarrow}_{cd}$ against the actual set of k-synchronous MSCs; any accepted MSC that violates causal delivery, or any k-synchronous MSC that is rejected, would disprove Lemma 1 and the reachability decidability theorem.","tokens_in":34304,"feed_emoji":"📨","tokens_out":6174,"duration_ms":62902,"temperature":0.7,"pith_summary":"This paper proves that two basic verification questions are decidable for k-synchronizable communicating systems: whether a given global state is reachable, and whether a given system is k-synchronizable in the first place. A system is k-synchronizable when every execution, up to reordering causally independent actions, can be split into rounds that start with at most k sends and end with at most k matching receives. The results hold for both mailbox communication, where each receiver has one FIFO queue, and peer-to-peer communication, where each pair of processes has private FIFO queues. Along the way, the paper corrects two earlier decidability proofs for mailbox automata that had produced false positives and false negatives.","feed_headline":"Reachability and k-synchronizability checks are decidable","feed_subtitle":"Finite-state abstractions make both questions checkable for mailbox and peer-to-peer automata.","key_machinery":"The central object is the extended conflict graph of an MSC, whose vertices are message exchanges and whose edges record causal order imposed by process timelines, message matching, and mailbox FIFO order. The paper augments this graph with per-process summary nodes $\\psi_p$ and two process sets $C_{S,p}$ and $C_{R,p}$, which carry across k-exchange boundaries exactly the information about unmatched sends needed to detect causal-delivery violations. The abstract transition relation $\\overset{e,k}{\\Longrightarrow}_{cd}$ updates these sets and rejects any k-exchange sequence whose extended conflict graph contains a cycle of the form $v \\xrightarrow{SS} v$. For membership, an instrumented system $S'$ adds a forwarding process $\\pi$, and the existence of a feasible bad execution is recognized by finite-state relations $\\overset{e,k}{\\Longrightarrow}_{feas}$ and $\\overset{e,k}{\\Longrightarrow}_{bad}$, reducing decidability to NFA emptiness.","core_discovery":"The central claim is that the set of k-synchronous message sequence charts (MSCs) of a communicating system is a regular language, and this regularity makes both reachability and k-synchronizability decidable. Concretely, the paper proves a graph-theoretic characterization: an MSC satisfying causal delivery is k-synchronous exactly when every strongly connected component of its conflict graph has size at most k and no RS edge lies on a cyclic path. It then builds finite-state abstract transition relations that recognize exactly the sequences of k-exchanges satisfying causal delivery, using summary nodes and per-process sets of causally affected senders and receivers. These abstractions yield decidability of reachability for k-synchronizable mailbox and peer-to-peer systems, and, with an instrumented system containing a special forwarding process, decidability of whether a given system is k-synchronizable.","pith_inferences":["The finite-state abstractions presented here translate directly into algorithms: one can build the automata for feasible and bad executions and test emptiness, though the paper does not analyze the resulting complexity.","The causal-delivery characterization via SS-cycles in the extended conflict graph likely transfers to other buffering disciplines, such as bags or per-sender queues, by adjusting only the graph rules in Figure 3.","The paper's closing conjecture, that forbidding linearisations that are not actual executions would simplify the development, suggests that the separate feasibility machinery might be absorbed into the reachability abstraction if the conjecture holds.","The peer-to-peer case needs only forbidden-sender sets rather than the richer summary-node structure, hinting that peer-to-peer k-synchronizability verification may be algorithmically lighter than mailbox verification."],"forward_implications":["Reachability of a global control state in any k-synchronizable mailbox or peer-to-peer system is decidable, even when some executions use buffers larger than k.","Deadlock-freedom, unspecified receptions, and absence of orphan messages become decidable for k-synchronizable systems, as noted in the paper's Remark 2.","Whether a given system is k-synchronizable is decidable for every k at least 1, in both mailbox and peer-to-peer settings.","The corrected characterization implies that earlier Hamiltonian-cycle-based algorithms for k-synchronizability are unsound, so verification tools must check SCC sizes and the absence of RS edges on cycles instead."],"supporting_citations":[{"why":"Introduced k-synchronizability, k-exchanges, and conflict graphs; the paper's theorems are framed as corrections of its flawed reachability and membership algorithms.","marker":"[4]"},{"why":"Supplies the regular model-checking viewpoint for bounded asynchrony, motivating the approach of recognizing k-synchronous behaviours as a regular language.","marker":"[5]"},{"why":"Provides the classical reduction idea of rescheduling executions by moving receive actions close to their sends, which underlies communication-closed rounds and k-synchronizability.","marker":"[14]"}],"fun_headline_variants":["Decidability proven for k-synchronizable systems","Fixing decidability proofs for k-sync automata","k-sync reachability and membership are decidable","Regular k-sync MSCs yield decidable checks"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument assumes that carrying only the two per-process sets $C_{S,p}$ and $C_{R,p}$ together with summary nodes from one k-exchange to the next preserves every causal-delivery violation that could arise between exchanges; if some cross-exchange dependency is invisible to these sets, the reachability decidability proof collapses.","fun_headline_variants_meta":{"raw":{"variants":["Decidability proven for k-synchronizable systems","Fixing decidability proofs for k-sync automata","k-sync reachability and membership are decidable","Regular k-sync MSCs yield decidable checks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000189,"raw_usage":{"total_tokens":1263,"prompt_tokens":798,"completion_tokens":465,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":414,"completion_tokens_details":{"reasoning_tokens":401}},"tokens_in":414,"tokens_out":465,"duration_ms":4578,"temperature":1.0,"reasoning_tokens":401,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:12:08.269383+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate all MSCs over a small system, say three processes and three messages with k=2, and compare the language accepted by the abstract transition relation $\\overset{e,k}{\\Longrightarrow}_{cd}$ against the actual set of k-synchronous MSCs; any accepted MSC that violates causal delivery, or any k-synchronous MSC that is rejected, would disprove Lemma 1 and the reachability decidability theorem.","supporting_citations":[],"review_version":1}