{"id":"31f8f58f-e03f-4853-b6f6-1c09b89e684b","arxiv_id":"1908.07282","paper_version":5,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Reachability, non-termination, unboundedness and related verification problems are NP-complete for flat FIFO machines, and reachability is NP-complete for flat lossy and flat front-lossy FIFO machines.","lead":"This paper determines the computational complexity of reachability and related verification problems for flat FIFO machines, showing they are NP-complete. It also constructs a counter-machine abstraction that makes LTL model checking decidable for this class of systems.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3.17 is internally inconsistent: it lists termination and boundedness as NP-complete even though the paper's own proofs establish NP-completeness for their complements, non-termination and unboundedness.","rationale":"The reader's conditional verdict is reasonable, and the lossy-to-front-lossy reduction gap they identify is real and should be fixed. However, that is not the most load-bearing concern I find. The most definite problem is that Theorem 3.17, the paper's summary theorem and the basis of the reader's strongest_claim, is internally inconsistent as written: it swaps the complement pairs. This is not a missing proof or a subtle semantic issue; it is a direct contradiction between the theorem statement and the paper's own definitions and upper/lower bound results. Because the intended results are clearly the 'un-' versions and those are proved, the fix is straightforward, so I would not escalate the verdict from conditional to reject. The Section 5 trace-flattening and order-machine concerns raised by the reader also reinforce conditionality, but the theorem statement error is more urgent because it makes a headline claim literally false. No ad hominem is intended; this is a statement-level correctness bug in an otherwise substantive paper.","tokens_in":29543,"tokens_out":31950,"duration_ms":348709,"concrete_test":"Re-read Theorem 3.17 against the problem definitions given earlier in Section 3 and the proofs immediately preceding it. For each predicate pair—(termination, non-termination), (boundedness, unboundedness), (channel-boundedness, channel-unboundedness), and (letter-channel-boundedness, letter-channel-unboundedness)—the paper proves membership and hardness only for the second, 'un-' version (Corollary 3.12, Proposition 3.15, Theorem 3.16), while the theorem lists exactly the complements. If the theorem is corrected to name non-termination, unboundedness, channel-unboundedness and letter-channel-unboundedness, the internal contradiction disappears; if it is left as written, the theorem asserts that both a problem and its complement are NP-complete, which would imply NP=coNP.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 3 defines the decision problems Non-termination (existence of an infinite run) and Unboundedness (infinite reachable set). Corollary 3.12 puts both in NP and Theorem 3.16 proves them NP-hard, so the paper has established that these problems are NP-complete. Termination is the complement of Non-termination over the same instances, and Boundedness is the complement of Unboundedness; similarly, channel-boundedness and letter-channel-boundedness are the complements of channel-unboundedness and letter-channel-unboundedness. Theorem 3.17 nevertheless states that 'termination, boundedness, channel-boundedness and letter-channel-boundedness are NP-complete.' If a coNP-complete problem, namely the complement of an NP-complete problem, were in NP, then NP would equal coNP. Thus the theorem as written is logically false under the standard assumption NP≠coNP, and in any case the paper gives no NP upper bound for the complement problems. The intended statement is clearly 'non-termination, unboundedness, channel-unboundedness and letter-channel-unboundedness,' matching the abstract and the surrounding proofs. This does not undermine the reachability and repeated-reachability NP-completeness results, but it makes the stated strongest claim incorrect verbatim and invalidates any direct citation of 'NP-complete termination/boundedness for flat FIFO machines.'","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies flat FIFO machines and establishes complexity results for reachability and related verification problems. In Section 3 it claims that reachability, repeated reachability, repeated control-state reachability, termination, boundedness, channel-boundedness, and letter-channel-boundedness are NP-complete for flat FIFO machines, with cyclicity decidable in linear time. Section 4 extends the reachability result to flat lossy and flat front-lossy FIFO machines, claiming NP-completeness. Section 5 constructs a synchronized product of counter machines that is weakly bisimilar to a given flat FIFO machine, asserts that this system is trace-flattable, and derives decidability of LTL model checking. The main proofs are based on reductions from 3SAT for lower bounds and on adaptations of prior work of Esparza-Ganty-Majumdar for upper bounds.","tokens_in":29821,"tokens_out":26016,"duration_ms":270499,"significance":"If the issues below are repaired, the paper makes a substantial contribution: it resolves the previously open complexity of reachability for flat FIFO machines, generalizes analogous results for flat counter machines, and provides a new counter-machine-based abstraction with potential applications to model checking. The paper contains several strong elements: an explicit 3SAT reduction covering six properties, a clean linear reduction from reachability to control-state reachability, and a nontrivial construction of a synchronized counter system. However, the significance is currently conditional on correcting the mismatched theorem statement, filling the missing lossy-to-front-lossy reduction, and supplying the missing details in the trace-flattening proof.","major_comments":[{"comment":"Theorem 3.17 states that 'termination, boundedness, channel-boundedness and letter-channel-boundedness are NP-complete,' but the proofs in Corollary 3.12 and Theorem 3.16 establish NP-completeness for the complementary problems non-termination, unboundedness, channel-unboundedness, and letter-channel-unboundedness. Since termination is the complement of non-termination over the same instances, and similarly for the other pairs, the theorem as stated would imply NP = coNP. The theorem should be corrected to state NP-completeness for the complement problems, matching the abstract and the surrounding proofs.","section":"§3, Theorem 3.17"},{"comment":"The NP upper bound for reachability in flat lossy FIFO machines relies on the unproved observation that 'control state reachability in flat lossy machines reduces to control state reachability in flat front-lossy machines.' This is a load-bearing step for Theorem 4.5: without a proof, the lossy upper bound is not established. The equivalence is plausible, but it is not immediate because the two semantics differ in which channel positions can be dropped, and the completed machine used in the reachability reduction must be shown to preserve the equivalence. A formal reduction and its correctness proof should be supplied.","section":"§4, after Lemma 4.4"},{"comment":"In the proof of Lemma 4.4 it is claimed that 'since the given front-lossy machine is flat, there is a bounded expression w over Δ whose language is the set of paths from q0 to q.' This is false for flat machines with branching: for example, an acyclic diamond with two distinct paths from q0 to q has a set of paths that is not a single bounded expression of the form w1* w2* ... wk*. The proof should instead enumerate or nondeterministically guess a path schema, as is done in [24], and apply Theorem 4.3 to the bounded expression of that schema.","section":"§4, Lemma 4.4"},{"comment":"The proof of Proposition 5.6 is only a sketch and does not provide a precise construction of the claimed trace-flattening S_flat. It refers to a 'paragraph preceding this lemma' that contains only intuition and a figure, not a formal definition. The induction step does not rigorously define what it means for a component to 'exit' a loop, how the sequentially composed machines are flat, or why the equality traces(Ssync) = f(traces(Sflat)) holds. Since Theorem 5.7 (LTL decidability) depends on this proposition, the construction and proof need to be completed or replaced with a citation to a result that supplies the missing details.","section":"§5, Proposition 5.6"}],"minor_comments":[{"comment":"The formal definition of front-lossy semantics omits the loss transition: it gives rules for send and receive transitions but no rule of the form (q, (a)_c · w) → (q, w). Since the prose says 'any letter at the front of any channel can be lost,' the loss transition should be added explicitly to the transition system.","section":"§4, semantics of front-lossy machines"},{"comment":"There are typos in this proof: 'bounded exression' should be 'bounded expression' and 'In our constrction' should be 'In our construction.'","section":"§4, proof of Lemma 4.4"},{"comment":"After modifying the order machines to remove τ-transitions, the paper says 'Now a proof similar to that of Proposition 5.4 can be used to show bisimulation.' This does not address why the modified order machines remain flat, especially in the case where merging states could destroy flatness, nor does it prove that the added guards preserve the bisimulation. More detail is needed.","section":"§5, modified synchronized system"},{"comment":"Corollary 3.9 describes the channel contents as the regular language w(c) · [z^{k-j}_c]^* when the loop is iterated, but this representation is undefined when x_c = ε. The statement should either exclude that case or explain how the empty-retrieval case is handled.","section":"§3, Corollary 3.9"}],"recommendation":"major_revision","confidential_remarks":"The paper is already published in LMCS 2020, but as a referee report on the manuscript I treat it as a submitted revision. The main results are likely correct after the stated corrections, but the mismatch in Theorem 3.17 and the missing proof of the lossy-to-front-lossy reduction are nontrivial and should be fixed. The trace-flattening argument also needs substantial completion. I do not see evidence of circularity; the lower bounds are genuine 3SAT reductions and the upper bounds build on prior results."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core result is real: reachability for flat FIFO machines is NP-complete, and the paper does the same for a cluster of related properties. The lower-bound proof is genuinely new because prior counter-machine reductions use binary encodings that do not transfer to FIFO channels; here a direct 3SAT reduction handles all the properties at once. The NP upper bounds are careful reductions to the Esparza–Ganty–Majumdar multipushdown result and to Papadimitriou's integer-programming lemma. The linear-time cyclicity test and the NP-completeness for flat lossy and front-lossy machines are also solid contributions. Lemma 3.8 on infinite iteration is fully proved in the text, even though it is also credited to earlier work—that is fine.\n\nThe main problem is a misstatement in Theorem 3.17. It lists termination, boundedness, channel-boundedness, and letter-channel-boundedness as NP-complete, but what the paper actually proves NP-complete are the negated properties: non-termination, unboundedness, channel-unboundedness, and letter-channel-unboundedness. Under standard complexity assumptions the complements cannot also be NP-complete, because that would collapse NP and coNP. This is almost certainly a naming slip—the abstract and the surrounding proofs use the correct names—but as printed the theorem is false, and anyone citing 'NP-complete termination for flat FIFO machines' would be citing something the paper does not establish. The reachability and repeated-reachability results are unaffected.\n\nTwo other soft spots, in proportion. The NP upper bound for flat lossy machines rests on an unproved one-sentence claim that control-state reachability in lossy machines reduces to front-lossy machines. I suspect the claim is true—front-loss is enough to expose the letters you need to read, and unwanted letters at the back can simply be ignored for control-state reachability—but a published paper should give a proof or a citation. The LTL decidability part, Theorem 5.7, is the shakiest: Proposition 5.6 is only a sketch, and the flat counter machine Sflat is never formally defined. If LTL decidability is a selling point, that section needs real work; if it is a bonus, it is acceptable as a construction idea.\n\nThis is a paper for verification researchers working on infinite-state systems, especially FIFO and counter machines. The main NP-completeness results are the kind of thing you want in a reference. It deserves a serious referee and, realistically, a revised version: fix the theorem statement, fill the lossy-to-front-lossy gap, and tighten Section 5. The substance is sound.","headline":"Solid NP-completeness results for flat FIFO machines, with a mislabeled theorem on termination/boundedness that should not be cited as-is.","tokens_in":30375,"tokens_out":4547,"would_cite":true,"duration_ms":46083,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q45","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"For flat FIFO machines—finite-state systems with unbounded message queues and at most one loop per state—reachability and six related verification problems are NP-complete, while cyclicity is decidable in linear time.","keywords":["flat FIFO machines","reachability","NP-completeness","lossy channel systems","flat counter machines","loop acceleration","trace-flattening","LTL model checking"],"falsifier":"Construct a flat lossy FIFO machine with one channel and a target control state, and compare reachable control states under ordinary lossy semantics (any message may vanish from anywhere) with those under front-lossy semantics (only the front message may vanish); a control state reachable in the first setting but not the second would refute the missing reduction behind Theorem 4.5. The same test can be run as a brute-force search over small machines to settle the lemma.","tokens_in":29245,"feed_emoji":"📨","tokens_out":9520,"duration_ms":82924,"temperature":0.7,"pith_summary":"Flat FIFO machines are finite-state systems with unbounded first-in first-out message channels whose control graph visits each state in at most one loop; they are the standard under-approximation for verifying general FIFO protocols. The paper closes a long-open question by proving that reachability, repeated reachability, repeated control-state reachability, non-termination, unboundedness, channel-unboundedness, and letter-channel-unboundedness are all NP-complete for flat FIFO machines, while cyclicity is decidable in linear time. It also proves reachability NP-complete for flat lossy and flat front-lossy machines, where messages may disappear. A final construction translates any flat FIFO machine into a trace-flattable synchronized system of counter machines that is weakly bisimilar to the original, making LTL model checking decidable and opening a route to a verification tool built on flat submachines.","feed_headline":"Flat FIFO reachability is NP-complete","feed_subtitle":"Unbounded queues collapse to counters, so flat-machine verification is NP-complete, not undecidable.","key_machinery":"The load-bearing identity is the word equation $x^\\omega = w y^\\omega$ of Lemma 2.4: for an elementary loop that reads $x_c$ and writes $y_c$ on channel $c$, infinite iterability forces the channel content to lie in $w(c)[z^{k-j}]^*$ for a primitive word $z$, turning the channel into a counter of blocks of $z$. This characterization drives the NP upper bounds, while the upper-bound algorithms themselves use the simulation of flat path schemas by multi-head pushdown automata restricted by bounded expressions and the linear reduction of reachability to control-state reachability. For model checking, the central construction is a synchronized system made of a counting abstraction machine and one order machine per channel, related to the original FIFO machine by a weak bisimulation and proved trace-flattable.","core_discovery":"On the paper's own terms, the discovery is that flatness makes unbounded FIFO channels behave like counters: the content of each channel along an infinitely iterated loop must settle into the periodic language $w(c)\\cdot[z^{k-j}]^*$, so all unbounded growth is exhausted by independent counter-like loops. From this, the paper claims that reachability has the same NP-complete complexity for flat FIFO machines as for flat counter machines, that the standard problems undecidable for general FIFO machines become NP-complete under flatness, and that reachability stays NP-complete when channels may lose messages. In addition, the paper constructs a synchronized product of counter machines, using a counting abstraction machine and order machines, that is weakly bisimilar to the given flat FIFO machine and trace-flattable; the reachability set of this counter system is semilinear, which yields decidability of LTL properties.","pith_inferences":["Because the paper's lower bound avoids binary counter encoding, the same 3SAT gadget should transfer to other flat models whose loop effects are unary, suggesting a general principle that flatness reduces unbounded queue or counter behavior to one-dimensional periodic growth.","The unproved reduction from lossy to front-lossy control-state reachability, if made fully rigorous, would imply that flat lossy verification only needs prefix constraints; a direct search over small flat machines comparing reachable control states under the two semantics could test this.","The bisimulation to a counter system suggests that branching-time model checking of flat FIFO machines might be attacked with existing counter-machine techniques, although the paper leaves CTL* explicitly open.","The periodic-channel characterization gives a small, explainable certificate for unboundedness—one loop plus one periodic word per channel—which could be surfaced to users of a future verification tool."],"forward_implications":["For flat FIFO machines, reachability, repeated reachability, repeated control-state reachability, termination, boundedness, channel-boundedness, and letter-channel-boundedness are all decidable and NP-complete; cyclicity is solvable in linear time.","Every loop that can be iterated infinitely acts on each channel as a counter over the periodic word $w(c)[z^{k-j}]^*$, so unboundedness is witnessed by a single loop whose effect is nonnegative on all channels and positive on at least one.","Reachability for flat lossy and flat front-lossy FIFO machines is NP-complete, in contrast to general lossy channel systems, where reachability is far beyond elementary.","LTL model checking of flat FIFO machines is decidable through the trace-flattable synchronized counter system, whose reachability set is semilinear.","The flat-submachine enumeration strategy used by counter-machine tools applies to general FIFO machines, terminating whenever some flat submachine shares the whole machine's reachability set."],"supporting_citations":[{"why":"Supplies the NP upper bound for control-state reachability of flat and single-path FIFO machines via multi-head pushdown automata and bounded expressions, the basis for Corollary 3.3 and Lemma 4.4.","marker":"[24]"},{"why":"Provides the linear reduction from reachability to control-state reachability for FIFO machines used in Proposition 3.1.","marker":"[37]"},{"why":"Supplies simple regular expressions and the quadratic computation of sigma-star(L) for lossy loops used in Theorem 4.1.","marker":"[1]"},{"why":"Provides the word-equation result (Lemma 2.4) and the well-abstracted transition-system viewpoint used to characterize infinitely iterable loops.","marker":"[28]"},{"why":"Gives symbolic loop acceleration for flat FIFO machines with CQDDs, the comparison point that Lemma 3.8 simplifies and extends to multiple channels.","marker":"[10]"},{"why":"Supplies the integer-programming lemma used to show unboundedness of a linear objective over feasible integer points in Proposition 3.15.","marker":"[34]"},{"why":"Defines trace-flattening and the preservation result used to derive LTL decidability from the synchronized counter system.","marker":"[18]"}],"fun_headline_variants":["Flat FIFO verification: NP-complete, just like counters","Flat queues: reachability collapses to counter complexity","Flat FIFO: NP-complete reachability, counters in disguise"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The NP upper bound for flat lossy FIFO machines rests on the paper's asserted but unproved reduction of control-state reachability under lossy semantics to the same question under front-lossy semantics; if the two semantics differ on some flat machine, the upper-bound half of Theorem 4.5 collapses.","fun_headline_variants_meta":{"raw":{"variants":["Flat FIFO verification: NP-complete, just like counters","Flat queues: reachability collapses to counter complexity","Flat FIFO: NP-complete reachability, counters in disguise"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000555,"raw_usage":{"total_tokens":2619,"prompt_tokens":898,"completion_tokens":1721,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":514,"completion_tokens_details":{"reasoning_tokens":1667}},"tokens_in":514,"tokens_out":1721,"duration_ms":14016,"temperature":1.0,"reasoning_tokens":1667,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T12:22:04.280011+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a flat lossy FIFO machine with one channel and a target control state, and compare reachable control states under ordinary lossy semantics (any message may vanish from anywhere) with those under front-lossy semantics (only the front message may vanish); a control state reachable in the first setting but not the second would refute the missing reduction behind Theorem 4.5. The same test can be run as a brute-force search over small machines to settle the lemma.","supporting_citations":[{"cited_title":"A perfect model for bounded verification","cited_arxiv_id":null,"evidence_quote":"Supplies the NP upper bound for control-state reachability of flat and single-path FIFO machines via multi-head pushdown automata and bounded expressions, the basis for Corollary 3.3 and Lemma 4.4."},{"cited_title":"Personal communication, 2018","cited_arxiv_id":null,"evidence_quote":"Provides the linear reduction from reachability to control-state reachability for FIFO machines used in Proposition 3.1."},{"cited_title":"On-the-fly analysis of systems with unbounded, lossy FIFO channels","cited_arxiv_id":null,"evidence_quote":"Supplies simple regular expressions and the quadratic computation of sigma-star(L) for lossy loops used in Theorem 4.1."},{"cited_title":"Purushothaman Iyer, and Gr´ egoire Sutre","cited_arxiv_id":null,"evidence_quote":"Provides the word-equation result (Lemma 2.4) and the well-abstracted transition-system viewpoint used to characterize infinitely iterable loops."},{"cited_title":"Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations","cited_arxiv_id":null,"evidence_quote":"Gives symbolic loop acceleration for flat FIFO machines with CQDDs, the comparison point that Lemma 3.8 simplifies and extends to multiple channels."},{"cited_title":"Papadimitriou","cited_arxiv_id":null,"evidence_quote":"Supplies the integer-programming lemma used to show unboundedness of a linear objective over feasible integer points in Proposition 3.15."},{"cited_title":"Demri, A","cited_arxiv_id":null,"evidence_quote":"Defines trace-flattening and the preservation result used to derive LTL decidability from the synchronized counter system."}],"review_version":1}