Regular Separability and Intersection Emptiness are Independent Problems

Georg Zetzsche; Ramanathan S. Thinniyam

REVIEW 1 major objections 4 minor 35 references

Regular Separability and Intersection Emptiness are Independent Problems

T0 review · 1 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Regular separability and intersection emptiness are independent problems: each can be decidable while the other is undecidable.

desk verdict A genuinely new independence result with a broken but repairable appendix proof. read the letter →

arxiv 1908.04038 v1 pith:JBFA43GG submitted 2019-08-12 cs.FL cs.LO

Ramanathan S. Thinniyam , Georg Zetzsche This is my paper · ORCID

classification cs.FLcs.LO MSC 68Q4503D0568Q17

keywords regularseparabilityintersectionemptinessdecidabilityincrementingautomataresetvectoradditionsystemshigher-orderpushdownpseudo-Rpredicatespower-H

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

This paper confronts the question whether regular separability—deciding if a regular language can sit between one input language and another—is just intersection emptiness in disguise. Earlier results on every language class where the question was settled showed the two problems decidable or undecidable together, suggesting a possible reduction. The paper refutes that suggestion by constructing two families of language classes: for incrementing automata whose final-counter predicates come from reset vector addition systems, intersection emptiness is decidable while regular separability is undecidable; for higher-order pushdown languages against incrementing automata with power predicates built from the same class, regular separability is decidable while intersection emptiness is undecidable. A fair reader should take away that the two problems are genuinely different and that no simple transfer from one to the other can exist under mild closure assumptions.

What carries the argument

The arguments run on three machines and one arithmetic logic. Reset vector addition systems (reset VASS) supply the first counterexample: their languages are closed under rational transductions, intersection, and union, emptiness is decidable, but infinity is undecidable. The class $I(\mathrm{pseudo}R)$ wraps them as predicates: an incrementing automaton reads a word while a counter only increases, and acceptance requires the final counter value to lie in a set $\nu(L)$ for some reset-VASS language $L$. For these classes, Lemma 4.5 is the load-bearing criterion: for unary languages $a^{S_0}, a^{S_1}$ with $\mathbb{N}\setminus 2\mathbb{N}\subseteq S_1$, regular separability holds exactly when $S_0$ is finite and disjoint from $S_1$, which turns separability into finiteness. Undecidability of infinity for reset VASS then makes $RS(I(\mathrm{pseudo}R),I(\mathrm{pseudo}R))$ undecidable, while a decision procedure for the positive existential arithmetic fragment $\Sigma^+_1(\mathbb{N},+,\le,1,\mathrm{pseudo}R)$—proved by showing every definable relation is effectively a pseudo-$R$ relation—makes intersection emptiness decidable. In the other direction, higher-order pushdown automata have decidable infinity but undecidable intersection, and Lemma 5.4 shows they can convert binary encodings into unary ones; together with Lemma 5.7 (regular separability is preserved by applying an inverse rational transduction) this yields decidable $RS(H,I(\mathrm{power}H))$ and undecidable $IE(H,I(\mathrm{power}H))$.

What would settle it

A reader could test the appendix's critical step by taking a pseudo-$R$ predicate $S$ and applying the proof to the formula $\exists y\,(S(y)\land x=y)$: if the projection relation cannot be realized by a reset VASS—or the construction provably fails—then Lemma 4.8 collapses and with it the decidability of $IE(I(\mathrm{pseudo}R),I(\mathrm{pseudo}R))$.

Watch

Extended reading notes

Core claim

The paper's central claim is that regular separability and intersection emptiness are independent decision problems, in the strong sense that neither can be reduced to the other. Concretely, Theorem 4.1 states that $RS(I(\mathrm{pseudo}R),I(\mathrm{pseudo}R))$ is undecidable while $IE(I(\mathrm{pseudo}R),I(\mathrm{pseudo}R))$ is decidable, where $I(\mathrm{pseudo}R)$ is the class of languages accepted by incrementing automata whose acceptance predicates are binary encodings $\nu(L)$ of reset-VASS languages. Theorem 5.2 states the reverse imbalance: $RS(H,I(\mathrm{power}H))$ is decidable while $IE(H,I(\mathrm{power}H))$ is undecidable, where $H$ is the class of all higher-order pushdown languages and $\mathrm{power}H$ stands for predicates of the form $\mathbb{N}\setminus 2\mathbb{N}\cup\{2^{\nu(w)}\mid w\in L\}$ with $L\in H$. If these theorems are right, the previously observed decidability correspondence between the two problems was an accident of the particular classes studied, not a general law.

Load-bearing premise

The decidability of intersection in the first counterexample rests on a formal induction claiming that every positive existential question about the natural numbers with predicates defined by reset vector addition systems can be answered by building another reset system; the appendix's crucial existential step swaps the two relations involved, so that induction is the load-bearing point that must be checked.

Editorial extensions

If this is right

In the class $I(\mathrm{pseudo}R)$, one can decide whether two languages intersect, yet cannot decide whether a regular certificate separates them; safety verification is therefore strictly easier than regular-certificate synthesis there.
In the pair $(H,I(\mathrm{power}H))$, one can always decide regular separability, so the obstruction to undecidability is not the existence of a separator but the intersection itself.
No general reduction between the two problems can exist merely because the language classes are full trios with decidable emptiness, since both counterexample families have those properties.
The paper's conclusion that the two problems are fundamentally different implies that any combinatorial characterization of regular separability must be incomparable with intersection emptiness.
The reduction from intersection emptiness to infinite intersection noted in the paper means the infinite-intersection problem is also not a common characterization of regular separability.

Reading between the lines

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

The same 'distort by encoding into numbers' recipe could be tried on other pairs of classes: take a class with decidable intersection but undecidable infinity and pass to $I(\mathrm{pseudo}C)$; the paper's reset-VASS instance suggests the dichotomy may reappear, for example with lossy channel systems, which the paper notes could replace reset VASS.
For the reverse direction, the construction is asymmetric and uses power predicates, which the paper itself calls contrived; a natural next target is a single symmetric class $\mathcal{C}$ with $RS(\mathcal{C},\mathcal{C})$ decidable and $IE(\mathcal{C},\mathcal{C})$ undecidable, or the mirror image.
Because Lemma 4.5 reduces regular separability to finiteness of a unary language, the hard core of regular separability undecidability may be infinity rather than disjointness; if so, classes with decidable infinity may admit decidable regular separability even when intersection is hard.
A testable extension would be to replace regular separators with other separator classes, such as piecewise testable or context-free languages, in the two constructions; the proofs lean on special properties of regular separators, so the independence result need not transfer.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Colleague,

The paper's main claim holds up: regular separability and intersection emptiness are not mutually reducible in general. The authors construct two new language classes, I(pseudoR) and I(powerH), and prove in Theorems 4.1 and 5.2 that one problem can be decidable while the other is undecidable. This directly refutes the correspondence that the recent literature had observed, and the classes are natural enough that the result feels like a genuine counterexample, not a contrivance.

What I like: the high-level arguments are clean and the building blocks (reset VASS, higher-order pushdown automata, rational transductions) are used cleverly. Lemma 4.5, the unary separator characterization, is simple and elegant. The reductions in Section 5 are also well done, and the paper is for the most part clearly written.

The soft spot is Appendix B, the proof of Lemma 4.8, which is the load-bearing decidability half of Theorem 4.1. As printed, the existential case is wrong. It says 'By induction hypothesis LR in R and since LR' is a homomorphic image of LR…', which reverses the actual direction: the induction hypothesis should give LR' in R, and LR is a projected image of LR'. Worse, the projection is not literally a homomorphism of the convolution language: erasing the eliminated coordinate leaves a suffix of all-padding columns if that word was strictly longest, and those columns must be removed by a rational transduction before closure under homomorphisms applies. The omission of this padding-elimination step is essential, because the definition of pseudo-R relation requires the exact convolution language. Lemma 4.10 then inherits the gap, so the decidability side of Theorem 4.1 depends on this fix.

That said, the intended argument is obvious and the repair is routine—compose the erasing homomorphism with a transducer that strips trailing padding columns, then invoke Lemma 4.3. I am fairly confident the result is true. There are also minor cross-reference errors (Lemma 4.6 cites Lemma 4.4 instead of 4.5) that should be caught by a careful referee.

The paper deserves a serious referee and likely acceptance after the appendix is fixed. I would cite it if I worked in this area, and I'd bring it to the reading group. The citation practice looks fine—the self-citations to [14] and [20] are appropriate.

Recommendation: send to peer review; the main theorems are novel and significant, and the flaw is in the writing, not the underlying idea.

Referee Report

1 major / 4 minor

Summary. The paper constructs two pairs of language classes showing that regular separability and intersection emptiness are independent decision problems. In Section 4, the class I(pseudoR), based on incrementing automata with reset-VASS predicates, is shown to have undecidable regular separability but decidable intersection emptiness (Theorem 4.1). In Section 5, the pair (H, I(powerH)) is shown to have decidable regular separability but undecidable intersection emptiness (Theorem 5.2). The proofs combine reductions from the infinity problem for reset VASS, a decidability argument for a positive existential logic over pseudo-R predicates, and a separation characterization for unary languages.

Significance. If the proof gap in Lemma 4.8 is repaired, the result is significant: it refutes the emerging intuition that regular separability and intersection emptiness are equivalent under mild closure assumptions. The constructions are natural, the paper gives explicit reductions and full appendix proofs, and it builds on independent external results (reset VASS boundedness undecidability, higher-order pushdown infinity decidability, context-free intersection undecidability). The main contribution is a family of counterexamples rather than a new algorithmic technique, but the counterexamples are well chosen and the high-level explanation in the conclusion is valuable.

major comments (1)

[Appendix B (Lemma 4.8), existential case] The existential step in the induction is not established as written. The text reads: 'By induction hypothesis LR in R and since LR′ is a homomorphic image of LR, Lemma 4.3 it tells us that LR′ belongs effectively to R.' This applies the induction hypothesis to LR, which is precisely the statement to be proved; the available induction hypothesis is LR′ ∈ R. Moreover, even after correcting the direction, the erasing homomorphism from LR′ to LR is not literally well defined: if the eliminated variable y has a longer binary representation than all remaining variables, erasing the y-track leaves a suffix of all-padding columns that is not part of the standard convolution of the projected tuple. The proof must first apply the erasing homomorphism and then compose with a rational transduction that deletes trailing all-padding columns, and only then invoke closure under rational transductions (Lemma 4.3). Because Lemma 4.8 underpins the decidability half of Theorem 4.1 via Lemma 4.10, this gap is load-bearing and must be repaired.

minor comments (4)

[Lemma 4.6, proof] The sentence 'By Lemma 4.4, K1 and K2 are regularly separable if and only if K1 is finite and disjoint from K2' should cite Lemma 4.5, which is the unary separability characterization; Lemma 4.4 states undecidability of the infinity problem for reset VASS.
[Lemma 4.10, final paragraph] The displayed formula defines φ2(y) via ∃x φ_T(x,y) ∧ S2(x), which describes membership in T aS2, but the preceding reduction concerns T aS1 ∩ aS2. Since intersection is symmetric, the resulting formula is correct (up to renaming of variables), but the text should state the direction explicitly and replace the apparent typo 'T aS2\aS1≠∅' with 'T aS2 ∩ aS1 ≠ ∅'.
[Lemma 4.5, proof] The phrase 'the language {a^x | 2^ℓ < x < 2^{ℓ+1}}⊆S1' is imprecise: the whole interval is not contained in S1 in general. Since 2N denotes the powers of two, the intended statement is that every x in that interval that is not a power of two belongs to S1, which is sufficient for the argument. Please rephrase to avoid ambiguity.
[Lemma 3.2, proof] There is a typo in 'the lanuage TL is accepted': it should be 'language'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: central claims rest on external results or self-contained proofs; the Appendix B induction typo and Lemma 4.5 gap are correctness issues, not circularity.

full rationale

The paper's main theorems are proved from independent, external results: undecidability of reset-VASS boundedness/infinity, decidability of reset-VASS emptiness, decidability of infinity for higher-order pushdown languages, and undecidability of context-free intersection. The only self-citation, Lemma 5.7 from the authors' unpublished reference [14], is used in the decidability proof of RS(H,I(powerH)), but the paper supplies a complete proof in Appendix E; the lemma is a parameter-free rational-transduction fact, so the citation is not load-bearing. Lemma 4.8's induction is deferred to Appendix B, and as printed the existential case interchanges the two relations ('By induction hypothesis LR∈R and since LR′ is a homomorphic image of LR...'); this is a proof-writing error rather than a circular derivation, because the intended hypothesis is on the subformula φ′, and the projection/erasure step requires closure of R under rational transductions, not an appeal to the target relation. The unary separability lemma (Lemma 4.5) also has a substantive proof gap that a correctness referee should examine, but that is a soundness issue, not an equivalence of a conclusion to its input. No fitted parameter is renamed as a prediction, no uniqueness theorem is imported from the authors' prior work, and no ansatz is smuggled in via citation. Therefore the paper exhibits no significant circularity.

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

The report has no free parameters because the paper is a pure existence proof with exact constructions. The audit lists the external decidability and undecidability results the counterexamples are built on, plus standard facts about unary regular languages and Parikh's theorem used in the proofs. The new predicate classes are mathematical definitions rather than empirical postulates, so they are listed as invented entities without independent evidence.

assumptions (7)

domain assumption Reset VASS coverability and emptiness are decidable.
Lemma 4.2, cited to [1,17]; underpins the Sigma+_1 truth procedure and hence IE decidability in Theorem 4.1.
domain assumption Reset VASS boundedness, and the derived infinity problem, are undecidable.
Lemma 4.4, cited to [15,24]; drives the RS undecidability reduction in Theorem 4.1.
domain assumption Infinity is decidable for higher-order pushdown languages.
Lemma 5.3, cited to [20]; needed to decide finiteness of L1 in RS(H,I(powerH)).
domain assumption Intersection emptiness for context-free languages is undecidable.
Used in Lemma 5.5 to prove IE(H,I(powerH)) undecidable.
standard math Every infinite regular language over a unary alphabet contains an arithmetic progression.
Used in Lemma 4.5 to prove the characterization of separability for a^S0 and a^S1.
domain assumption The class H of higher-order pushdown languages is effectively closed under rational transductions, a full trio.
Used in Lemma 5.8 to reduce T^{-1}L1 back to H after applying Lemma 5.7.
standard math Parikh's theorem gives semilinear representations for the Parikh images of regular and context-free languages.
Used in Lemma 4.10 to express a rational transduction over a^* as a formula in Sigma+_1(N,+,<=,1,pseudoR).

invented entities (3)

Incrementing automata over a predicate class I(P)
purpose: Machine model used to define the counterexample language classes C1,D1,C2,D2.
A new mathematical definition, not an empirical entity; its value is internal to the proof.
pseudo-R predicates
purpose: Predicates nu(L) for reset VASS languages L; used to make intersection decidable while separability undecidable.
Mathematical construction; no external falsifiable prediction.
power-H predicates
purpose: Predicates N\2N union {2^nu(w) | w in L} for L in H; used to make separability decidable while intersection undecidable.
Mathematical construction; no external falsifiable prediction.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Regular Separability and Intersection Emptiness are Independent Problems." pith.science (2026). https://pith.science/paper/JBFA43GG

@misc{pith2026190804038,
  author       = {Pith},
  title        = {Pith review of: Regular Separability and Intersection Emptiness are Independent Problems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JBFA43GG}},
  note         = {Machine review of arXiv:1908.04038}
}

abstract

The problem of \emph{regular separability} asks, given two languages $K$ and $L$, whether there exists a regular language $S$ with $K\subseteq S$ and $S\cap L=\emptyset$. This problem has recently been studied for various classes of languages. All the results on regular separability obtained so far exhibited a noteworthy correspondence with the intersection emptiness problem: In eachcase, regular separability is decidable if and only if intersection emptiness is decidable. This raises the question whether under mild assumptions, regular separability can be reduced to intersection emptiness and vice-versa. We present counterexamples showing that none of the two problems can be reduced to the other. More specifically, we describe language classes $\mathcal{C_1}$, $\mathcal{D_1}$, $\mathcal{C_2}$, $\mathcal{D_2}$ such that (i)~intersection emptiness is decidable for $\mathcal{C_1}$ and $\mathcal{D_1}$, but regular separability is undecidable for $\mathcal{C_1}$ and $\mathcal{D_1}$ and (ii)~regular separability is decidable for $\mathcal{C_2}$ and $\mathcal{D_2}$, but intersection emptiness is undecidable for $\mathcal{C_2}$ and $\mathcal{D_2}$.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 34 canonical work pages

[14]

An approach to regular separability in vector addition systems

Wojciech Czerwi\' n ski and Georg Zetzsche. An approach to regular separability in vector addition systems. 2019. In preparation

work page 2019
[20]

Luke Ong

Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In POPL 2016 , pages 151--163, New York, NY, USA, 2016. ACM

work page 2016
[1]

General decidability theorems for infinite-state systems

Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science , pages 313--321. IEEE, 1996

work page 1996
[2]

Some algorithmic problems for pseudovarieties

Jorge Almeida. Some algorithmic problems for pseudovarieties. Publ. Math. Debrecen , 54(1):531--552, 1999

work page 1999
[3]

Transductions and context-free languages

Jean Berstel. Transductions and context-free languages . Springer-Verlag, 2013

work page 2013
[4]

Automatic structures

Achim Blumensath and Erich Gradel. Automatic structures. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332) , pages 51--62. IEEE, 2000

work page 2000
[5]

Finite presentations of infinite structures: Automata and interpretations

Achim Blumensath and Erich Gr \"a del. Finite presentations of infinite structures: Automata and interpretations. Theory of Computing Systems , 37(6):641--674, 2004

work page 2004
[6]

It is undecidable if two regular tree languages can be separated by a deterministic tree-walking automaton

Miko aj Boja \' n czyk. It is undecidable if two regular tree languages can be separated by a deterministic tree-walking automaton. Fundam. Inform. , 154(1-4):37--46, 2017

work page 2017

Show all 35 references

[7]

A generic approach to the static analysis of concurrent programs with procedures

Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal of Foundations of Computer Science , 14(04):551--582, 2003

2003
[8]

Separability of rational relations in A ^* ^m by recognizable relations is decidable

Christian Choffrut and Serge Grigorieff. Separability of rational relations in A ^* ^m by recognizable relations is decidable. Information processing letters , 99(1):27--32, 2006

2006
[9]

Regular separability of Parikh automata

Lorenzo Clemente, Wojciech Czerwi\' n ski, S awomir Lasota, and Charles Paperman. Regular separability of Parikh automata. In Proceedings of ICALP '17 , pages 117:1--117:13, 2017

2017
[10]

Separability of reachability sets of vector addition systems

Lorenzo Clemente, Wojciech Czerwi\' n ski, S awomir Lasota, and Charles Paperman. Separability of reachability sets of vector addition systems. In Proceedings of STACS '17 , pages 24:1--24:14, 2017

2017
[11]

Regular separability of one counter automata

Wojciech Czerwi\' n ski and S awomir Lasota. Regular separability of one counter automata. In Proceedings of LICS '17 , pages 1--12, 2017

2017
[12]

Narayan Kumar, and Prakash Saivasan

Wojciech Czerwi \'n ski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular separability of well-structured transition systems. In Proceedings of CONCUR '18 , pages 35:1--35:18, 2018. http://dx.doi.org/10.4230/LIPIcs.CONCUR.2018....

2018 doi
[13]

A characterization for decidable separability by piecewise testable languages

Wojciech Czerwi\' n ski, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A characterization for decidable separability by piecewise testable languages. Discrete Mathematics & Theoretical Computer Science , 19(4), 2017

2017
[15]

Reset nets between decidability and undecidability

Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings , pages 103--115, 1998

1998
[16]

A mathematical introduction to logic

Herbert Enderton and Herbert B Enderton. A mathematical introduction to logic . Elsevier, 2001

2001
[17]

Fundamental structures in well-structured infinite transition systems

Alain Finkel and Philippe Schnoebelen. Fundamental structures in well-structured infinite transition systems. In LATIN '98: Theoretical Informatics, Third Latin American Symposium, Campinas, Brazil, April, 20-24, 1998, Proceedings , pages 102--118, 1998

1998
[18]

Gool and Benjamin Steinberg

Samuel J.v. Gool and Benjamin Steinberg. Pointlike sets for varieties determined by groups. Advances in Mathematics , 348:18--50, 2019

2019
[19]

Deciding piecewise testable separability for regular tree languages

Jean Goubault - Larrecq and Sylvain Schmitz. Deciding piecewise testable separability for regular tree languages. In Proceedings of ICALP '16 , pages 97:1--97:15, 2016

2016
[21]

Context-free languages and turing machine computations

Juris Hartmanis. Context-free languages and turing machine computations. In Proceedings of Symposia in Applied Mathematics , volume 19, pages 42--51, 1967

1967
[22]

Hunt III

Harry B. Hunt III. On the decidability of grammar problems. Journal of the ACM , 29(2):429--447, 1982

1982
[23]

Regular separability of one counter automata

S awomir Lasota and Wojciech Czerwi \'n ski. Regular separability of one counter automata. Logical Methods in Computer Science , 15, 2019. Extended version of LICS 2017 paper

2019
[24]

Undecidable problems in unreliable computations

Richard Mayr. Undecidable problems in unreliable computations. Theoretical Computer Science , 297(1-3):337--354, 2003

2003
[25]

On context-free languages

Rohit J Parikh. On context-free languages. Journal of the ACM (JACM) , 13(4):570--581, 1966

1966
[26]

Separating regular languages with two quantifiers alternations

Thomas Place. Separating regular languages with two quantifiers alternations. In Proceedings of LICS '15 , pages 202--213, 2015

2015
[27]

Separating regular languages by piecewise testable and unambiguous languages

Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In Proceedings of MFCS '13 , pages 729--740, 2013

2013
[28]

Separation and the successor relation

Thomas Place and Marc Zeitoun. Separation and the successor relation. In Proceedings of STACS '15 , pages 662--675, 2015

2015
[29]

Separating regular languages with first-order logic

Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Logical Methods in Computer Science , 12(1), 2016

2016
[30]

Concatenation hierarchies: New bottle, old wine

Thomas Place and Marc Zeitoun. Concatenation hierarchies: New bottle, old wine. In Proceedings of CSR '17 , pages 25--37, 2017

2017
[31]

Separation for dot-depth two

Thomas Place and Marc Zeitoun. Separation for dot-depth two. In Proceedings of LICS '17 , pages 1--12, 2017

2017
[32]

The covering problem

Thomas Place and Marc Zeitoun. The covering problem. Logical Methods in Computer Science , 14(3), 2018

2018
[33]

Szymanski and John H

Thomas G. Szymanski and John H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing , 5(2), 1976

1976
[34]

An approach to computing downward closures

Georg Zetzsche. An approach to computing downward closures. In Proceedings of ICALP '15 , pages 440--451, 2015

2015
[35]

Separability by piecewise testable languages and downward closures beyond subwords

Georg Zetzsche. Separability by piecewise testable languages and downward closures beyond subwords. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 , pages 929--938, 2018

2018

Pith tools

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

[1] [14]

An approach to regular separability in vector addition systems

Wojciech Czerwi\' n ski and Georg Zetzsche. An approach to regular separability in vector addition systems. 2019. In preparation

work page 2019

[2] [20]

Luke Ong

Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In POPL 2016 , pages 151--163, New York, NY, USA, 2016. ACM

work page 2016

[3] [1]

General decidability theorems for infinite-state systems

Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science , pages 313--321. IEEE, 1996

work page 1996

[4] [2]

Some algorithmic problems for pseudovarieties

Jorge Almeida. Some algorithmic problems for pseudovarieties. Publ. Math. Debrecen , 54(1):531--552, 1999

work page 1999

[5] [3]

Transductions and context-free languages

Jean Berstel. Transductions and context-free languages . Springer-Verlag, 2013

work page 2013

[6] [4]

Automatic structures

Achim Blumensath and Erich Gradel. Automatic structures. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332) , pages 51--62. IEEE, 2000

work page 2000

[7] [5]

Finite presentations of infinite structures: Automata and interpretations

Achim Blumensath and Erich Gr \"a del. Finite presentations of infinite structures: Automata and interpretations. Theory of Computing Systems , 37(6):641--674, 2004

work page 2004

[8] [6]

It is undecidable if two regular tree languages can be separated by a deterministic tree-walking automaton

Miko aj Boja \' n czyk. It is undecidable if two regular tree languages can be separated by a deterministic tree-walking automaton. Fundam. Inform. , 154(1-4):37--46, 2017

work page 2017