{"id":"f30f4f37-f5ee-4cf9-b22a-95cedb4360ab","arxiv_id":"2411.14067","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Under the Strong Exponential Time Hypothesis, simulation preorder and simulation equivalence cannot be decided in O(n^{2-epsilon}) time, so simulation is inherently quadratic.","lead":"This paper proves that, assuming a standard complexity conjecture called SETH, checking whether one process's behavior can be simulated by another must take about quadratic time in the worst case. It gives formal evidence that simulation is harder than bisimulation, which matters for software and hardware verification tools.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified; the reduction is sound and the imported SETH-hardness theorem is standard.","rationale":"The central claim is a conditional lower bound: under SETH, no O(n^{2-eps}) algorithm for deterministic simulation preorder or for simulation equivalence on LTSs. I checked the two reduction steps that are original to this paper. For Theorem 6, the relation R = { (delta_A(q0,w), delta_B(q0,w)) : w in Sigma* } union { (top_A, top_B) } witnesses the reverse direction when L(A) subset of L(B), since every accepting A-state along a word is matched by an accepting B-state and both tops are dead. For the forward direction, if alpha(A) is simulated by alpha(B), then any w in L(A) reaches an accepting A-state whose check-transition must be matched by a check-transition in B, so w in L(B). Thus language inclusion is exactly captured. The complement construction in Theorem 7 is the standard reduction from intersection emptiness to inclusion. Corollary 9's gadget is also correct: s has a-transitions to s0 and t0 while t only has an a-transition to t0, so s is simulated by t exactly when s0 is simulated by t0, and t is always simulated by s via the identity on t0. Therefore s and t are simulation equivalent exactly when s0 is simulated by t0. The constant-factor state increases do not affect the exponent. The sole external dependency is Wehar's SETH-hardness of 2-DFA-NEI, which is cited, published, and not contradicted by any known algorithm; conditional lower bounds in this area routinely import such results. I found no internal inconsistency, no missing case in the reductions, and no reason to disturb the reader's ACCEPT verdict.","tokens_in":6530,"tokens_out":20286,"duration_ms":220513,"concrete_test":"Verify [19, Theorem 7.21] against the peer-reviewed DLT version [4] (or independently re-prove the CNF-SAT-to-2-DFA-NEI construction), and independently re-run Theorem 6 on exhaustive small DFAs comparing alpha(A) subset of alpha(B) with L(A) subset of L(B). If the imported theorem is confirmed, the quadratic lower bound stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"No significant objection identified. The original step (Theorem 6) is correct: alpha maps language inclusion to simulation by encoding acceptance as a fresh check-transition to a dead state, and the converse holds because deterministic transitions can be matched prefix-by-prefix. The complement reduction in Theorem 7 and the one-state nondeterministic gadget in Corollary 9 are also sound. The only exposed dependency is the quoted SETH-hardness of 2-DFA-NEI from [19, Theorem 7.21]; this is a standard published fine-grained result, and the paper flags it as imported. I found no internal inconsistency or missing step that would alter the verdict.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proves conditional fine-grained lower bounds for simulation preorder and simulation equivalence. Assuming the Strong Exponential Time Hypothesis (SETH), it shows that deciding similarity on deterministic labelled transition systems requires time Ω(n^{2−ε}) for every ε>0, and that deciding simulation equivalence on general LTSs also requires Ω(n^{2−ε}) time. The proof reduces the SETH-hard problem 2-DFA-NEI to simulation preorder via a linear-time transformation α that adds a special check transition from accepting states, and then reduces deterministic simulation preorder to simulation equivalence via a two-state nondeterministic gadget. The main results are Theorem 6 (language inclusion iff α-simulation), Theorem 7 (transfer from simulation to intersection emptiness), Corollary 8 (deterministic preorder lower bound), and Corollary 9 (equivalence lower bound).","tokens_in":6594,"tokens_out":8172,"duration_ms":70253,"significance":"If the result holds, it settles a natural open question in the fine-grained complexity of process-theoretic equivalences: simulation preorder and equivalence are inherently quadratic in the worst case under SETH, matching the best known quadratic upper bounds. The paper cleanly separates simulation from bisimilarity from a fine-grained perspective, since bisimilarity admits near-linear algorithms. The reductions are simple, transparent, and easy to verify by hand; the α construction is elegant and the two-state gadget is correct. The only external dependency is the SETH-hardness of 2-DFA-NEI, which is a published result and is explicitly flagged as imported. The paper is concise and well organized.","major_comments":[],"minor_comments":[{"comment":"The displayed example formula is written as Ψ = (x1 ∨ x2) ∧ (x1 ∨ x2); as printed this is equivalent to x1 ∨ x2 and does not illustrate the split-half construction described in the surrounding text, which presumably intends a clause over the first half and a complementary clause over the second half.","section":"Section 2, example formula"},{"comment":"In the definition of a DFA, the final-state set is written F ⊆ Q, but Q has not been introduced; it should be F ⊆ S, and the initial state should be q0 ∈ S.","section":"Definition 1"},{"comment":"The statement says that 2-DFA-NEI for input DFAs of n states is computable in f(n) + O(n) steps, but the constructed LTSs each have n+1 states, so the correct expression is f(2n+2) + O(n) unless n is redefined as the total number of states; the asymptotic conclusion is unaffected.","section":"Theorem 7"},{"comment":"The complement DFA is written as 'B' rather than \\overline{B}, and the proof should note that if B is not already complete, a sink state must be added; this is harmless for the complexity bound but should be stated.","section":"Proof of Theorem 7"},{"comment":"The constructed LTS is written as a triple (S1 ∪ S2 ∪ {s,t}, −→1 ∪ −→2 ∪ ...), but an LTS is a four-tuple requiring an action set and an initial state; the intended construction is clear from Fig. 2 but should be defined completely.","section":"Corollary 9"},{"comment":"The bound 'mn2^{1/2 n}' is ambiguous; it should be written as m·n·2^{n/2} to clearly indicate the product structure.","section":"Section 2, size bound"},{"comment":"The authors attribute Theorem 3 to the PhD thesis [19, Theorem 7.21]; since the peer-reviewed DLT 2020 paper [4] also covers these results, they should cite both sources for this theorem to ease verification.","section":"Theorem 3 attribution"}],"recommendation":"minor_revision","confidential_remarks":"The paper is very short and the central proof is correct. The main external dependency is the fine-grained hardness of 2-DFA-NEI, quoted from a PhD thesis [19]; the authors already cite the peer-reviewed version [4] in the introduction, but they should make the attribution in Theorem 3 explicit for both sources. I also suggest adding a sentence or two of proof for Theorem 6, as it is the core novelty, even though the argument is straightforward. Overall the paper fits the journal well and the result is publishable after these minor corrections."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the paper is right. The reductions are sound, the imported SETH-hardness theorem is standard, and the result closes a natural open question. I agree with the reader's ACCEPT.\n\nThe genuinely new piece is the alpha encoding: a deterministic LTS built from a DFA by adding a check transition from accepting states to a fresh dead state, which makes language inclusion coincide with simulation preorder. That's a simple but effective bridge between automata theory and concurrency. The complement step (Theorem 7) turns intersection-emptiness into inclusion, and the one-state nondeterministic gadget (Corollary 9) lifts the lower bound from similarity to simulation equivalence. I checked the directions; they work.\n\nThe soft spots are small. The entire lower bound inherits from Wehar's 2-DFA-NEI theorem, quoted from a PhD thesis without reproof. That's acceptable given the citation, but it means the paper is a conditional result with one imported dependency. The proof of Theorem 6 is asserted as 'easy to see' rather than spelled out; a referee will want the explicit simulation relation, even though it is straightforward. There are also a few typos ('Not that' for 'Note that', mangled indices in Section 2). None of this changes the verdict.\n\nThe citation pattern is honest. The authors' earlier bisimulation lower bound is cited for context, not used, and the reduction itself is not in the cited fine-grained automata papers. This is a new result, not a repackaging.\n\nFor whom: anyone working on fine-grained complexity of process-theoretic problems, or on simulation algorithms. It's a short, checkable paper deserving a serious referee; I'd expect it accepted after minor revisions. I'd cite it and bring it to a reading group.","headline":"A sound, short reduction showing SETH forces quadratic time for simulation preorder and equivalence; minor presentation nits only.","tokens_in":7135,"tokens_out":4398,"would_cite":true,"duration_ms":42041,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","68Q45","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Under SETH, simulation preorder and equivalence both require quadratic time.","keywords":["simulation preorder","simulation equivalence","Strong Exponential Time Hypothesis","fine-grained complexity","quadratic lower bound","DFA intersection non-emptiness","labelled transition systems","bisimulation"],"falsifier":"Check the reduction on two small DFAs whose languages are known to be one contained in the other: translate them with $\\alpha$ and run a simulation checker, which must return true. A mismatch on any pair of DFAs would refute Theorem 6. Alternatively, finding any algorithm that decides similarity on deterministic LTSs in $O(n^{2-\\epsilon})$ time would, through the paper's translation, solve 2-DFA-NEI in $O(n^{2-\\epsilon})$ and thereby disprove SETH.","tokens_in":6313,"feed_emoji":"⏱️","tokens_out":14904,"duration_ms":128274,"temperature":0.7,"pith_summary":"The paper is a conditional lower-bound proof about simulation, the standard process-theoretic relation in which one state simulates another if every move of the first can be matched by the second. It argues that if the Strong Exponential Time Hypothesis (SETH) is true, then deciding the simulation preorder on deterministic labelled transition systems, and simulation equivalence on general labelled transition systems, cannot be done in time $O(n^{2-\\epsilon})$ for any $\\epsilon>0$, where $n$ is the number of states. This would make the known quadratic upper bounds tight and mean simulation is inherently quadratic. The argument works by a linear translation from pairs of deterministic finite automata to transition systems, so the known SETH-based hardness of checking whether two automata accept a common word carries over unchanged.","feed_headline":"No subquadratic simulation check can exist unless SETH falls","feed_subtitle":"A linear reduction from automaton intersection shows any faster simulation algorithm would refute SETH.","key_machinery":"The load-bearing construction is the translation $\\alpha$ from a DFA $A=(Q,\\Sigma,\\delta,F,q_0)$ to a deterministic LTS with state set $Q\\cup\\{\\top\\}$, a fresh action $\\checkmark$, all original transitions $(q,a,\\delta(q,a))$, and an extra transition $(q,\\checkmark,\\top)$ for every accepting state $q\\in F$. This makes acceptance observable as a $\\checkmark$-move to a sink, so one automaton's language being contained in another becomes a simulation obligation. The second gadget, used for equivalence, adds two fresh states $s,t$ with $s\\xrightarrow{a}s_0$, $s\\xrightarrow{a}t_0$, and $t\\xrightarrow{a}t_0$; it forces $s\\simeq t$ to hold exactly when $s_0\\sqsubseteq t_0$, turning preorder hardness into equivalence hardness.","core_discovery":"The central claim is that simulation inherits a quadratic lower bound from the automaton intersection problem. Concretely, for any two DFAs $A$ and $B$, the paper builds deterministic LTSs $\\alpha(A)$ and $\\alpha(B)$ by adding a fresh accepting sink and a special $\\checkmark$ action on final states; then $L(A)\\subseteq L(B)$ holds exactly when $\\alpha(A)$ is simulated by $\\alpha(B)$ (Theorem 6). Since deciding $L(A)\\cap L(B)=\\emptyset$ is the same as a language containment against the complement automaton, any $f(n)$-time algorithm for simulation on deterministic LTSs yields an $f(n)+O(n)$-time algorithm for 2-DFA-NEI (Theorem 7). With the known SETH lower bound for 2-DFA-NEI, this gives Corollaries 8 and 9; the equivalence case adds one nondeterministic branching gadget so that equivalence checking on general LTSs is exactly as hard as preorder checking on deterministic LTSs.","pith_inferences":["The same encoding should transfer the quadratic lower bound to other behavioural preorders that can express regular language inclusion through a linear gadget, such as trace inclusion or failures inclusion; the paper only hints at this universality.","If SETH is accepted as a working hypothesis, the result is a practical warning: worst-case simulation instances for general LTSs are intrinsically dense, so subquadratic tool behaviour must come from exploiting sparsity or special structure.","The reduction's linearity yields a benchmarking recipe: converting random DFA pairs via $\\alpha$ produces simulation instances that are hard under SETH, which can show how far practical algorithms are from the theoretical worst case."],"forward_implications":["Under SETH, the known quadratic upper bounds for simulation preorder become tight: no $O(n^{2-\\epsilon})$ algorithm exists for deterministic LTSs.","Under SETH, simulation equivalence on general nondeterministic LTSs is also not decidable in $O(n^{2-\\epsilon})$ time, even though on deterministic systems equivalence coincides with bisimilarity and is nearly linear.","Any future subquadratic simulation algorithm would automatically give a subquadratic algorithm for 2-DFA-NEI, which is known to contradict SETH.","The result sharpens the contrast with bisimilarity: simulation becomes fundamentally harder in the worst case under a standard complexity assumption."],"supporting_citations":[{"why":"Supplies Theorem 3, the SETH-based quadratic hardness of 2-DFA-NEI that the whole simulation lower bound inherits.","marker":"[19]"},{"why":"Defines SETH and ETH, the complexity hypothesis under which the conditional lower bound is stated.","marker":"[10]"},{"why":"Establishes the fine-grained hardness of finite-automaton intersection that motivates and supports the imported 2-DFA-NEI bound.","marker":"[4]"}],"fun_headline_variants":["Simulation checks are quadratic unless SETH collapses","No faster simulation without SETH falling","Simulation lower bound ties to SETH","Quadratic simulation bound from SETH","Simulation inherently quadratic under SETH"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole lower bound rests on the imported theorem that, under SETH, deciding whether two deterministic automata with $n$ states accept a common word takes time essentially quadratic in $n$; the paper does not reprove that theorem, so if it is flawed the simulation lower bound collapses.","fun_headline_variants_meta":{"raw":{"variants":["Simulation checks are quadratic unless SETH collapses","No faster simulation without SETH falling","Simulation lower bound ties to SETH","Quadratic simulation bound from SETH","Simulation inherently quadratic under SETH"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000138,"raw_usage":{"total_tokens":1077,"prompt_tokens":789,"completion_tokens":288,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":405,"completion_tokens_details":{"reasoning_tokens":224}},"tokens_in":405,"tokens_out":288,"duration_ms":3393,"temperature":1.0,"reasoning_tokens":224,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:35:06.338658+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Check the reduction on two small DFAs whose languages are known to be one contained in the other: translate them with $\\alpha$ and run a simulation checker, which must return true. A mismatch on any pair of DFAs would refute Theorem 6. Alternatively, finding any algorithm that decides similarity on deterministic LTSs in $O(n^{2-\\epsilon})$ time would, through the paper's translation, solve 2-DFA-NEI in $O(n^{2-\\epsilon})$ and thereby disprove SETH.","supporting_citations":[{"cited_title":"On the complexity of intersection non-emptiness problems","cited_arxiv_id":null,"evidence_quote":"Supplies Theorem 3, the SETH-based quadratic hardness of 2-DFA-NEI that the whole simulation lower bound inherits."}],"review_version":1}