Pith. sign in

REVIEW 1 major objections 3 minor 34 references

On the Reachability Problem for Two-Dimensional Branching VASS

T0 review · 1 major / 3 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Every two-dimensional branching vector addition system has a computable semilinear reachability set, making its reachability problem decidable.

desk verdict Strong result, repairable gap: the termination proof as written has a hole in Lemma D.6 that the authors need to fix before I'd sign off on it. read the letter →

arxiv 2506.22561 v1 pith:QEFPLOYP submitted 2025-06-27 cs.LO cs.FL

Clotilde Bizière , Thibault Hilaire , Jérôme Leroux , Grégoire Sutre This is my paper · ORCID
classification cs.LOcs.FL MSC 68Q8568Q60
keywords branchingvectoradditionsystemsreachabilityproblemsemilinearsetsPetrinetstwo-dimensionalBVASSdecidabilitycycleaccelerationconestabilization
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 proves that every two-dimensional branching vector addition system (a Petri-net-like model where transitions may merge configurations by summing them) has a reachability set that is semilinear: a finite union of linear sets, presented explicitly by an algorithm. This makes the reachability problem decidable in dimension two, extending the classical result for ordinary two-dimensional VASS and the known one-dimensional branching case. A sympathetic reader should care because exact reachable sets, rather than over-approximations, are not usually available for such expressive models; the proof shows how cycle acceleration can be made retroactive without losing termination.

What carries the argument

The central object is an algorithmic exploration: an acyclic node-labeled graph where each node n is labeled by (a_n, q_n, z_n, P_n), with P_n a periodic subset of $N^{2}$ obtained by the cycle-acceleration step P_n := Add^*_{I_n}(∑_{m→n} P_m). The iterable set I_n collects n-elementary vectors (displacements of elementary cycles available from ancestors) and n-consecutive vectors (differences of base vectors of same-state ancestors). The termination argument's geometric engine is the v-stabilization of a cone C⊆$Q^{2}$_≥0, defined as (C + Q_≥0 v) ∩ $Q^{2}$_≥0, together with the h-mode of a cone, which tracks which non-positive vectors stabilize it; Lemma 7.2 says h-modes stabilize along non-decreasing cone chains, and Lemma 7.3 decomposes every elementary vector of a descendant node into earlier elementary vectors, ancestor periodic sets, and consecutive vectors.

What would settle it

Exhibit a 2-BVASS and an execution of Explore that produces an infinite sequence of non-redundant nodes not covered by ancestors; equivalently, find a primary and directed algorithmic exploration whose periodic sets P_n do not stabilize, for instance whose global cone Con(⋃_n P_n) is not finitely generated. Lemma 7.4 and Corollary 7.10 assert no such exploration exists, so a concrete search over small 2-BVASS instances for such an infinite exploration would settle the claim.

Watch

Extended reading notes

Core claim

The central claim is Theorem 7.11: for every 2-BVASS B, the reachability set JBK is semilinear and a presentation is computable from B. The algorithm Explore builds a finite acyclic exploration whose nodes carry (state, base vector, periodic set) labels; soundness and completeness show the union of the node sets equals JBK, and termination is proved by contradiction. Assuming an infinite exploration exists, the authors extract an infinite primary and directed sub-exploration, interpret the acceleration step geometrically as v-stabilization of cones in $Q^{2}$_≥0, prove the global cone is finitely generated via a decomposition of elementary-cycle vectors, and then use a Dickson-style argument to force a redundant non-leaf node, contradicting non-redundancy.

Load-bearing premise

The proof's termination depends on Lemma 7.3, which asserts that in every primary and directed algorithmic exploration, the elementary-cycle vectors of any descendant node decompose into a finite sum of earlier elementary vectors, periodic sets outside the main descendant set, and consecutive vectors; this relies on the stabilization of h-modes and on a carefully chosen node n1. If that decomposition fails, the global cone cannot be shown finitely generated, and the contradiction forcing finite exploration collapses.

Editorial extensions

If this is right

  • The reachability problem for 2-BVASS is decidable: given an initial and a target configuration, one can compute the semilinear presentation and test membership.
  • The reachability set of a 2-BVASS is effectively semilinear, so reachability questions reduce to Presburger arithmetic in dimension two.
  • The decidability frontier for BVASS reachability moves from dimension one to dimension three, which remains open.
  • The acyclic exploration with retroactive cycle acceleration provides a template for exact forward analysis of branching models, not merely coverability approximations.

Reading between the lines

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

  • The paper gives no complexity bound; a natural next question is the size of the computed semilinear presentation, which may grow non-elementarily even though the algorithm terminates.
  • The primary and directed core-witness lemma in Section 6 is a general statement about infinite spannable graphs and may be reusable to prove termination of other worklist-based symbolic algorithms that build infinite acyclic graphs.
  • The two-dimensional cone machinery (axes, h-modes, v-stabilization) exploits Q^2_≥0 in an essential way; extending the result to dimension three would require a new geometric invariant, since the stabilizer of a cone is no longer a cone in higher dimensions.
  • Because branching transitions can be instantiated using reachable configurations, the algorithm's acceleration is retroactive—cycles discovered later pump earlier nodes; similar retroactive acceleration could be tried for other branching or pushdown generalizations, but termination would need a new argument outside dimension two.
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

1 major / 3 minor

Summary. This paper claims that the reachability set of every two-dimensional branching vector addition system (2-BVASS) is semilinear and that a semilinear presentation is computable from the system, thereby settling the reachability problem for this class. The proposed algorithm Explore builds a finite acyclic exploration graph whose nodes carry semilinear sets of configurations; Section 5 proves that the explorations produced are sound and complete. The termination proof extracts an infinite primary and directed sub-exploration from any infinite run, shows that the cone spanned by all periods is finitely generated via a mode-stabilization argument and a decomposition of elementary cycle vectors, and derives a contradiction from non-redundancy. Detailed proofs are deferred to an appendix.

Significance. If the proof is correct, this is a substantial advance: it is the first decidability result for branching VASS beyond dimension one and a natural generalization of the Hopcroft--Pansiot theorem for classical 2-VASS. The algorithm is constructive and the proof does not rely on fitting parameters or on the decidability of BVASS reachability. The paper is generally well written and the appendix is detailed, with the soundness and completeness parts argued carefully. However, the termination proof contains a load-bearing gap in Lemma D.6 that needs to be repaired; the manuscript should therefore not be accepted in its current form.

major comments (1)
  1. [Section 7.2 / Appendix D.2 (Lemma D.6)] The proof constructs transitions t_j of V_{n'0} by replacing each background node m of a transition of V_n by lambda(m) in Nmin. This is valid only when every lambda(m) is a strict ancestor of n'0, because V_{n'0} is the instantiation with F_{n'0} = {q_s(z_s) | s ->+ n'0}. The text only guarantees lambda(m) ->* n'0. If n'0 is in Nmin, which can happen when Nmin is a singleton, then lambda(m)=n'0 for all m in Des(n0), and q_{n'0}(z_{n'0}) is not an element of F_{n'0}; hence the constructed t_j need not be transitions of V_{n'0}, and theta need not be a cycle of V_{n'0}. Consequently the conclusion that the displacement v of theta lies in some E_m with n'0 ->* m ->* n1 does not follow. This affects Lemma 7.3, and through it Lemma 7.7 and the finite-generation of Con(P_N), so it is load-bearing for the termination proof. The gap appears repairable: since the exploration is primary and infinite, every node has a proper descendant, so n'0 can be chosen as a common descendant of Nmin union (N \ Des(n0)) that is not itself in Nmin; then every lambda(m) is a strict ancestor of n'0. The manuscript must be revised to make this choice and the strictness explicit.
minor comments (3)
  1. [Abstract and Section 1] "Vectors addition systems" should be "Vector addition systems" in the abstract and in the first paragraph of the introduction.
  2. [Appendix D.2, proof of Lemma D.6] The variables s_j and s'_j are used in the display v' = v + sum_{j=1}^k (z_{s'_j} - z_{s_j}) but are never defined; in addition, the two displayed formulas for v and v' appear to be interchanged relative to the definitions of b_j and t_j. Please rewrite this paragraph with explicit indexing of the multiset M_j.
  3. [Section 7.4, proof of Lemma 7.9] The phrase "by by m \preceq n" contains a duplicated word and should read "by m \preceq n".

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the 2-BVASS semilinearity proof is constructive and self-contained, with external classical results carrying the only imported support.

full rationale

This paper derives a computable semilinear presentation of the reachability set of every 2-BVASS from a constructive algorithm (Explore) whose partial correctness is proved in Section 5 and whose termination is proved in Section 7. No fitted parameter is renamed as a prediction, and no theorem from the authors' prior work is invoked as the forcing premise. The load-bearing external results are classical and independent: Hopcroft and Pansiot's theorem for 2-VASS [19], Lemma 2.1 relating finitely-generated periodic sets and cones, and Lemma A.3; none of these assumes semilinearity or decidability of BVASS reachability, and none is authored by the present authors. The self-citations [12, 13, 25, 27] appear only as related-work context and are not used to justify the central construction. Soundness and completeness are established directly from the algorithm's invariants, and termination is proved by contradiction using primary and directed explorations, cone modes, and cycle decomposition, without assuming the target result. The skeptic's concern about Lemma D.6, regarding the choice of n0' when it is the unique minimal node, is a potential correctness gap rather than a circularity: it does not make the theorem equivalent to its inputs, and the gap is presented as repairable. Accordingly, no circular step can be exhibited, and the appropriate circularity score is 0.

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

No parameters are fitted to data. The proof rests on standard background (Dickson, König, Presburger) and on two cited lemmas from Hopcroft and Pansiot [19] that are external to the present claim. Fact 3.4 is an unproved but standard pumping lemma. No new physical or computational entities are postulated.

assumptions (6)
  • standard math Dickson's Lemma: the product order on N^k is well-quasi-ordered
    Used in Lemma 7.9 to show that the relation m⪯n defined by q_m=q_n and z_m≤z_n is a wqo, yielding an infinite chain with equal states and non-decreasing vectors.
  • standard math König's Lemma: every infinite finitely-branching forest has an infinite branch
    Used in Remark 5.3 and in Lemma 6.1/Lemma C.3 to extract branches and minimal branches from finitely-branching spanning forests.
  • standard math Lemma 2.1 from Hopcroft and Pansiot [19]: P⊆Z^d periodic is finitely generated iff Con(P) is a finitely generated cone
    Used in Lemma 4.4 and in Section 7 to transfer finite-generation between periodic sets and cones.
  • standard math Lemma A.3 from [19]: if B+P⊆x+Con(P) for finitely generated P and infinite B⊆Z^d, then B+P=B'+P for some finite B'⊆B
    Used in Lemma 7.9 to obtain two chain nodes with z_n_j∈z_n_i+P, producing the redundancy contradiction.
  • domain assumption Fact 3.4: an elementary cycle of an instantiated VASS can be pumped from any configuration with all coordinates at least the iteration constant c
    Stated without proof in Section 3 and used in Claim B.3 to prove soundness (E_n⊆F_n). It is a standard cycle-pumping property but is not derived in the paper.
  • standard math Effectiveness of semilinear-set operations and Presburger arithmetic (inclusion, intersection, finite generation)
    Used in Corollary A.13 and Lemma 4.4 to compute finite spanning sets for Add*_I(Per(G)) and to decide the termination condition of the iterative computation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the Reachability Problem for Two-Dimensional Branching VASS." pith.science (2026). https://pith.science/paper/QEFPLOYP

@misc{pith2026250622561,
  author       = {Pith},
  title        = {Pith review of: On the Reachability Problem for Two-Dimensional Branching VASS},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QEFPLOYP}},
  note         = {Machine review of arXiv:2506.22561}
}
read the original abstract

Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there exists a run from an initial configuration to a final one. This problem has been known to be decidable for over forty years, and its complexity has recently been precisely characterized. Our work concerns the reachability problem for BVASS, a branching generalization of VASS. In dimension one, the exact complexity of this problem is known. In this paper, we prove that the reachability problem for 2-dimensional BVASS is decidable. In fact, we even show that the reachability set admits a computable semilinear presentation. The decidability status of the reachability problem for BVASS remains open in higher dimensions.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 13 canonical work pages

  1. [1]

    Approximating petri net reachability along context-free traces

    Mohamed Faouzi Atig and Pierre Ganty. Approximating petri net reachability along context-free traces. In Supratik Chakraborty and Amit Kumar, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India , volume 13 of LIPIcs , pages 152--163. Schloss Dagstuhl - Le...

    work page doi:10.4230/lipics.fsttcs.2011.152 2011

  2. [2]

    The reachability problem for two-dimensional vector addition systems with states

    Michael Blondin, Matthias Englert, Alain Finkel, Stefan G \" o ller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. J. ACM , 68(5):34:1--34:43, 2021. https://doi.org/10.1145/3464794 doi:10.1145/3464794

    doi:10.1145/3464794 2021

  3. [3]

    Two-variable logic on data trees and XML reasoning

    Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. In Stijn Vansummeren, editor, Proceedings of the Twenty-Fifth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 26-28, 2006, Chicago, Illinois, USA , pages 10--19. ACM , 2006. https://doi.org/10....

    work page arXiv 2006

  4. [4]

    Analysis of recursively parallel programs

    Ahmed Bouajjani and Michael Emmi. Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst. , 35(3):10:1--10:49, 2013. https://doi.org/10.1145/2518188 doi:10.1145/2518188

    doi:10.1145/2518188 2013

  5. [5]

    The tractability border of reachability in simple vector addition systems with states

    Dmitry Chistikov, Wojciech Czerwinski, Filip Mazowiecki, Lukasz Orlikowski, Henry Sinclair - Banks, and Karol Wegrzycki. The tractability border of reachability in simple vector addition systems with states. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024 , pages 1332--1354. IEEE , 2024. h...

    arXiv 2024

  6. [6]

    Timed pushdown automata and branching vector addition systems

    Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017 , pages 1--12. IEEE Computer Society, 2017. https://doi.org/10.1109/LICS.2017.8005083 doi:10.1109/LICS.2017.8005083

    work page arXiv 2017

  7. [7]

    Murawski, and C

    Conrad Cotton - Barratt, Andrzej S. Murawski, and C. - H. Luke Ong. ML and extended branching VASS . In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings ...

    doi:10.1007/978-3-662-54434-1 2017

  8. [8]

    The reachability problem for P etri nets is not elementary

    Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, J \' e r \^ o me Leroux, and Filip Mazowiecki. The reachability problem for P etri nets is not elementary. J. ACM , 68(1):7:1--7:28, 2021. https://doi.org/10.1145/3422822 doi:10.1145/3422822

    doi:10.1145/3422822 2021

Show all 34 references
  1. [9]

    David and H

    R. David and H. Alla. Continuous petri nets. In Proc. of the 8th European Workshop on Application and Theory of Petri Nets, Zaragoza, Spain, 1987 , 1987

    1987

  2. [10]

    Vector addition tree automata

    Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automata. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings , pages 64--73. IEEE Computer Society, 2004. https://doi.org/10.1109/LICS.2004...

    2004 arXiv

  3. [11]

    The covering and boundedness problems for branching vector addition systems

    St \' e phane Demri, Marcin Jurdzinski, Oded Lachish, and Ranko Lazic. The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. , 79(1):23--38, 2013. https://doi.org/10.1016/J.JCSS.2012.04.002 doi:10.1016/J.JCSS.2012.04.002

    2013 doi

  4. [12]

    Polynomial-space completeness of reachability for succinct branching VASS in dimension one

    Diego Figueira, Ranko Lazic, J \' e r \^ o me Leroux, Filip Mazowiecki, and Gr \' e goire Sutre. Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th I...

    2017

  5. [13]

    Reachability for two-counter machines with one test and one reset

    Alain Finkel, J \' e r \^ o me Leroux, and Gr \' e goire Sutre. Reachability for two-counter machines with one test and one reset. In Sumit Ganguly and Paritosh K. Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Scie...

    2018 doi

  6. [14]

    Complexity analysis of continuous petri nets

    Est \' baliz Fraca and Serge Haddad. Complexity analysis of continuous petri nets. Fundam. Informaticae , 137(1):1--28, 2015. https://doi.org/10.3233/FI-2015-1168 doi:10.3233/FI-2015-1168

    2015 doi

  7. [15]

    Reachability in bidirected pushdown VASS

    Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Sch \" u tze, and Georg Zetzsche. Reachability in bidirected pushdown VASS . In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ...

    2022 doi

  8. [16]

    Seymour Ginsburg and Edwin H. Spanier. Semigroups, P resburger formulas and languages. Pacific Journal of Mathematics , 16(2):285--296, 1966. https://doi.org/10.2140/pjm.1966.16.285 doi:10.2140/pjm.1966.16.285

    1966 doi

  9. [17]

    A polynomial-time algorithm for reachability in branching VASS in dimension one

    Stefan G \" o ller, Christoph Haase, Ranko Lazi\'c, and Patrick Totzke. A polynomial-time algorithm for reachability in branching VASS in dimension one. In ICALP , volume 55 of LIPIcs , pages 105:1--105:13. Schloss Dagstuhl, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.105 ...

    2016 doi

  10. [18]

    A survival guide to presburger arithmetic

    Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News , 5(3):67--82, 2018. https://doi.org/10.1145/3242953.3242964 doi:10.1145/3242953.3242964

    2018

  11. [19]

    Hopcroft and Jean - Jacques Pansiot

    John E. Hopcroft and Jean - Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. , 8:135--159, 1979. https://doi.org/10.1016/0304-3975(79)90041-0 doi:10.1016/0304-3975(79)90041-0

    1979 doi

  12. [20]

    Fo2( , +1, ) on data trees, data tree automata and branching vector addition systems

    Florent Jacquemard, Luc Segoufin, and Jer \' e mie Dimino. Fo2( , +1, ) on data trees, data tree automata and branching vector addition systems. Log. Methods Comput. Sci. , 12(2), 2016. https://doi.org/10.2168/LMCS-12(2:3)2016 doi:10.2168/LMCS-12(2:3)2016

    2016 doi

  13. [21]

    Karp and Raymond E

    Richard M. Karp and Raymond E. Miller. Parallel Program Schemata . J. Comput. Syst. Sci. , 3(2):147--195, 1969. https://doi.org/10.1016/S0022-0000(69)80011-5 doi:10.1016/S0022-0000(69)80011-5

    1969 doi

  14. [22]

    The reachability problem for vector addition systems with a stack is not elementary

    Ranko Lazic. The reachability problem for vector addition systems with a stack is not elementary. CoRR , abs/1310.1767, 2013. https://doi.org/10.48550/arXiv.1310.1767 doi:10.48550/arXiv.1310.1767

    2013 doi arXiv

  15. [23]

    Ranko Lazic, Thomas Christopher Newcomb, Jo \" e l Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. Fundam. Informaticae , 88(3):251--274, 2008. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi88-3-03

    2008

  16. [24]

    Nonelementary complexities for branching VASS , MELL , and extensions

    Ranko Lazi\'c and Sylvain Schmitz. Nonelementary complexities for branching VASS , MELL , and extensions. ACM Trans. Comput. Log. , 16(3):20:1--20:30, 2015. https://doi.org/10.1145/2733375 doi:10.1145/2733375

    2015 doi

  17. [25]

    The reachability problem for P etri nets is not primitive recursive

    J \' e r \^ o me Leroux. The reachability problem for P etri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022 , pages 1241--1252. IEEE , 2021. https://doi.org/10.1109/FOCS52979.20...

    2021

  18. [26]

    Reachability in vector addition systems is primitive-recursive in fixed dimension

    J \' e r \^ o me Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019 , pages 1--13. IEEE , 2019. https:...

    2019

  19. [27]

    On the coverability problem for pushdown vector addition systems in one dimension

    J \' e r \^ o me Leroux, Gr \' e goire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Magn \' u s M. Halld \' o rsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Progr...

    2015 doi

  20. [28]

    Counting and equality constraints for multitree automata

    Denis Lugiez. Counting and equality constraints for multitree automata. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of...

    2003 doi

  21. [29]

    Ernst W. Mayr. An algorithm for the general petri net reachability problem. SIAM J. Comput. , 13(3):441--460, 1984. https://doi.org/10.1137/0213029 doi:10.1137/0213029

    1984 doi

  22. [30]

    Reachability for bounded branching VASS

    Filip Mazowiecki and Michal Pilipczuk. Reachability for bounded branching VASS . In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands , volume 140 of LIPIcs , pages 28:...

    2019 doi

  23. [31]

    Beyond regularity: Equational tree automata for associative and commutative theories

    Hitoshi Ohsaki. Beyond regularity: Equational tree automata for associative and commutative theories. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedi...

    2001 doi

  24. [32]

    Multiset-valued linear index grammars: Imposing dominance constraints on derivations

    Owen Rambow. Multiset-valued linear index grammars: Imposing dominance constraints on derivations. In James Pustejovsky, editor, 32nd Annual Meeting of the Association for Computational Linguistics, 27-30 June 1994, New Mexico State University, Las Cruces, New Mexico, USA, Pro...

    1994

  25. [33]

    On the computational complexity of dominance links in grammatical formalisms

    Sylvain Schmitz. On the computational complexity of dominance links in grammatical formalisms. In Jan Hajic, Sandra Carberry, and Stephen Clark, editors, ACL 2010, Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics, July 11-16, 2010, Uppsal...

    2010

  26. [34]

    Karp-miller trees for a branching extension of VASS

    Kumar Neeraj Verma and Jean Goubault - Larrecq. Karp-miller trees for a branching extension of VASS . Discret. Math. Theor. Comput. Sci. , 7(1):217--230, 2005. https://doi.org/10.46298/DMTCS.350 doi:10.46298/DMTCS.350

    2005 doi

Pith tools

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