Pith. sign in

REVIEW 7 minor 22 references

A Quadratic Lower Bound for Simulation

T0 review · 0 major / 7 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Under SETH, simulation preorder and equivalence both require quadratic time.

desk verdict A sound, short reduction showing SETH forces quadratic time for simulation preorder and equivalence; minor presentation nits only. read the letter →

arxiv 2411.14067 v1 pith:OIAVEJRI submitted 2024-11-21 cs.LO

Jan Friso Groote , Jan Martens This is my paper · ORCID
classification cs.LO MSC 68Q1768Q2568Q4568Q60
keywords simulationpreorderequivalenceStrongExponentialTimeHypothesisfine-grainedcomplexityquadraticlowerboundDFAintersectionnon-emptinesslabelledtransitionsystemsbisimulation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 7 minor

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).

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.

minor comments (7)
  1. [Section 2, example formula] 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.
  2. [Definition 1] 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.
  3. [Theorem 7] 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.
  4. [Proof of Theorem 7] 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.
  5. [Corollary 9] 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.
  6. [Section 2, size bound] The bound 'mn2^{1/2 n}' is ambiguous; it should be written as m·n·2^{n/2} to clearly indicate the product structure.
  7. [Theorem 3 attribution] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the simulation lower bound follows by a genuine reduction from the externally established SETH-hard problem 2-DFA-NEI, not by assuming or renaming the target result.

full rationale

The derivation chain is a standard fine-grained reduction. The paper imports the SETH-hardness of 2-DFA-NEI from Wehar's thesis ([19, Theorem 7.21]), which is external to the authors and is not derived from simulation complexity. The central step is Theorem 6, where the mapping alpha adds a fresh acceptance-check transition to each automaton and proves L(A) subseteq L(B) iff alpha(A) is simulated by alpha(B). This is a genuine reduction between two distinct relations, not a restatement: similarity is defined on LTSs via the simulation game, while language inclusion is defined via accepted words, and the encoding of accepting states as fresh check transitions is the substantive bridge. The construction is explicit and checkable, and the paper's own equations exhibit the reduction. Theorem 7 then composes this reduction with complementation to show that an O(f(n)) simulation algorithm would solve 2-DFA-NEI in O(f(n)+n), and Corollary 8 applies the imported SETH hardness. Corollary 9's one-state nondeterministic gadget is likewise a standard reduction from similarity to simulation equivalence, with the equivalence s ≃ t iff s0 ⊑ t0 argued directly from the added transitions. The only self-citation, [7], appears in the introduction as context about bisimulation lower bounds and is not used in the proof of the simulation lower bound. No fitted parameter is renamed as a prediction, no uniqueness theorem is imported from the authors' prior work, and no known result is merely renamed. The exposed dependency on the quoted SETH-hardness theorem is an external, published, parameter-free result, so it constitutes independent support rather than circularity. The verdict is no significant circularity.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No fitted values or hand-tuned constants appear in the paper. The central claim depends on SETH and on the established SETH-hardness of 2-DFA-NEI from Wehar's thesis. The paper introduces only proof gadgets, such as the fresh accepting state and check label in the alpha construction, which are syntactic reductions and carry no independent-evidence burden.

assumptions (3)
  • domain assumption Strong Exponential Time Hypothesis (SETH): CNF-SAT with n variables cannot be solved in O(2^{delta n}) for any delta < 1.
    Explicitly assumed in the abstract and Section 1; all lower bounds are conditional on it.
  • domain assumption 2-DFA-NEI has no O(n^{2-epsilon}) algorithm under SETH (Wehar's thesis Theorem 7.21; de Oliveira Oliveira and Wehar, DLT 2020).
    The paper's Theorem 3 restates this result and the simulation lower bound inherits from it; the theorem is cited, not proved.
  • domain assumption The CNF-SAT-to-DFA construction in Section 2 preserves satisfiability and produces automata with O(m n 2^{n/2}) states.
    This construction is needed to convert an O(N^{2-epsilon}) 2-DFA-NEI algorithm into a subexponential CNF-SAT algorithm; details are referenced to [19].

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Quadratic Lower Bound for Simulation." pith.science (2026). https://pith.science/paper/OIAVEJRI

@misc{pith2026241114067,
  author       = {Pith},
  title        = {Pith review of: A Quadratic Lower Bound for Simulation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OIAVEJRI}},
  note         = {Machine review of arXiv:2411.14067}
}
read the original abstract

We show that deciding simulation equivalence and simulation preorder have quadratic lower bounds assuming that the Strong Exponential Time Hypothesis holds. This is in line with the best know quadratic upper bounds of simulation equivalence. This means that deciding simulation is inherently quadratic. A typical consequence of this result is that computing simulation equivalence is fundamentally harder than bisimilarity.

Figures

Figures reproduced from arXiv: 2411.14067 by the authors.

Figure 1
Figure 1. Automata accepting L Ψ 1 (left), and L Ψ 2 (right) for Ψ = (x1 ∨ x2) ∧ (x1 ∨ x2). 3 SETH implies simulation has quadratic com￾plexity In this section we show that determining simulation preorder on deterministic, and simulation equivalence on non-deterministic transition systems is necessarily quadratic, assuming SETH is valid. Simulation is typically defined on labelled transition systems which divert slightly from… view at source ↗
Figure 2
Figure 2. The LTS M. On deterministic structures simulation equivalence coincides with bisimilar￾ity. Meaning that deciding simulation equivalence on deterministic structures can be done in almost linear time [9, 6, 16], where ‘almost’ refers to a mul￾tiplicative factor with the inverse Ackermann’s function. However, using one non-deterministic transition a faster than quadratic algorithm for simulation equivalence on LTSs in… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 13 canonical work pages

  1. [1]

    Transformational design an d implementation of a new efficient solution to the ready sim- ulation problem

    Bard Bloom and Robert Paige. Transformational design an d implementation of a new efficient solution to the ready sim- ulation problem. Sci. Comput. Program. , 24(3):189–220, 1995. doi:10.1016/0167-6423(95)00003-B. 7

    doi:10.1016/0167-6423(95)00003-b 1995

  2. [2]

    Simulation-based minim azation

    Doron Bustan and Orna Grumberg. Simulation-based minim azation. ACM Trans. Comput. Log., 4(2):181–206, 2003. doi:10.1145/635499.635502

    work page arXiv 2003

  3. [3]

    Saving space in a time efficient simulation algorithm

    Silvia Crafa, Francesco Ranzato, and Francesco Tapparo . Saving space in a time efficient simulation algorithm. Fundam. Informaticae, 108(1-2):23–42,

    work page

  4. [4]

    On the fine grained com- plexity of finite automata non-emptiness of intersection

    Mateus de Oliveira Oliveira and Michael Wehar. On the fine grained com- plexity of finite automata non-emptiness of intersection. I n Natasa Jonoska and Dmytro Savchuk, editors, Developments in Language Theory - 24th International Conference, DLT 2020, Tampa, FL, USA, May 11-15 , 2020, Proceedings, volume 12086 of Lecture Notes in Computer Science , pages 6...

    doi:10.1007/978-3-030-48516-0 2020

  5. [5]

    Problems on finite auto mata and the exponential time hypothesis

    Henning Fernau and Andreas Krebs. Problems on finite auto mata and the exponential time hypothesis. Algorithms, 10(1):24, 2017

    work page 2017

  6. [6]

    Michael J. Fischer. Efficiency of equivalence algorithms . In Raymond E. Miller and James W. Thatcher, editors, Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York , USA, The IBM Research Symposia Series, pages 153–167. Plenum Pr ess, New York,...

    doi:10.1007/978-1-4684-2001-2 1972

  7. [7]

    Jan Friso Groote, Jan Martens, and Erik P. de Vink. Lowerb ounds for bisimulation by partition refinement. Log. Methods Comput. Sci. , 19(2), 2023. URL: https://doi.org/10.46298/lmcs-19(2:10)2023, doi:10.46298/LMCS-19(2:10)2023

    doi:10.46298/lmcs-19(2:10)2023 2023

  8. [8]

    Henzinger, and Peter W

    Monika Rauch Henzinger, Thomas A. Henzinger, and Peter W . Kopke. Computing simulations on finite and infinite graphs. In 36th Annual Symposium on Foundations of Computer Science, Milwaukee, W isconsin, USA, 23-25 October 1995 , pages 453–462. IEEE Computer Society, 1995. doi:10.1109/SFCS.1995.492576

    work page arXiv 1995

Show all 22 references
  1. [9]

    Hopcroft and Richard M

    John E. Hopcroft and Richard M. Karp. A linear algorithm f or testing equivalence of finite automata. Tr 114, Cornell University, 1971

    1971

  2. [10]

    On the compl ex- ity of k-SAT

    Russell Impagliazzo and Ramamohan Paturi. On the compl ex- ity of k-SAT. Journal of Computer and System Sciences , 2001. doi:10.1006/jcss.2000.1727

    2001

  3. [11]

    Lower bounds for natural proof systems

    Dexter Kozen. Lower bounds for natural proof systems. I n Proceedings of SFCS 1977 , pages 254–266. IEEE, IEEE, 1977. doi:10.1109/SFCS.1977.16

    1977 doi

  4. [12]

    Antonín Kucera and Richard Mayr. Why is simulation hard er than bisim- ulation? In Lubos Brim, Petr Jancar, Mojmír Kretínský, and A ntonín Kucera, editors, CONCUR 2002 - Concurrency Theory, 13th International 8 Conference, Brno, Czech Republic, August 20-23, 2002, Proce edings...

    2002

  5. [13]

    An algebraic definition of simulation bet ween pro- grams

    Robin Milner. An algebraic definition of simulation bet ween pro- grams. In D. C. Cooper, editor, Proceedings of the 2nd Interna- tional Joint Conference on Artificial Intelligence. London, U K, Septem- ber 1-3, 1971 , pages 481–489. William Kaufmann, 1971. URL: http://ijcai.org...

    1971

  6. [14]

    An efficient simulation algorithm on kripke structures

    Francesco Ranzato. An efficient simulation algorithm on kripke structures. Acta Informatica , 51(2):107–125,

  7. [15]

    A new efficient simulation equivalence algorithm

    Francesco Ranzato and Francesco Tapparo. A new efficient simulation equivalence algorithm. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proce edings, pages 171–180. IEEE Computer Society, 2007. doi:10.1109/LICS.2007.8

    2007 doi

  8. [16]

    Robert E. Tarjan. Efficiency of a good but not linear set un ion algorithm. Journal of the ACM (JACM) , 22(2):215–225, 1975. doi:10.1145/321879.321884

    1975

  9. [17]

    van Glabbeek and Bas Ploeger

    Rob J. van Glabbeek and Bas Ploeger. Correcting a space- efficient sim- ulation algorithm. In Aarti Gupta and Sharad Malik, editors , Com- puter Aided Verification, 20th International Conference, CAV 2 008, Princeton, NJ, USA, July 7-14, 2008, Proceedings , volume 5123 of Lecture...

    2008 doi

  10. [18]

    Hardness of Easy Probl ems: Basing Hard- ness on Popular Conjectures such as the Strong Exponential T ime Hypoth- esis

    Virginia Vassilevska Williams. Hardness of Easy Probl ems: Basing Hard- ness on Popular Conjectures such as the Strong Exponential T ime Hypoth- esis. In Thore Husfeldt and Iyad Kanj, editors, Proceedings of IPEC 2015 , volume 43 of Leibniz International Proceedings in Informa...

    2015 doi

  11. [19]

    On the complexity of intersection non-emptiness problems

    Michael Wehar. On the complexity of intersection non-emptiness problems . PhD thesis, University at Buffalo, 2016. 9

    2016

  12. [2002]

    doi:10.1007/3-540-45694-5\_39

    doi

  13. [2011]

    doi:10.3233/FI-2011-412

    2011 doi

  14. [2014]

    URL: https://doi.org/10.1007/s00236-014-0195-9 , doi:10.1007/S00236-014-0195-9

    doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.