Pith. sign in

REVIEW 4 minor 41 references

Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants

T0 review · 0 major / 4 minor · reviewed 2026-07-13 · grok-4.5

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

Pith's one-line read If a configuration is unreachable in a branching vector addition system, a semilinear inductive invariant separates it, so reachability is decidable by enumeration.

desk verdict They close the 30-year BVAS reachability problem with a clean forward-only invariant construction; the math is fully written out and the amalgamation dependency is internal, not soft. read the letter →

arxiv 2607.09558 v1 pith:WBH5KATL submitted 2026-07-10 cs.LO cs.FL

Clotilde Bizière , Jérôme Leroux , Grégoire Sutre This is my paper · ORCID
classification cs.LOcs.FL MSC 68Q6003B2568Q85
keywords branchingvectoradditionsystemsreachabilityproblemsemilinearinductiveinvariantsattractorswell-structuredmultiplicativeexponentiallinearlogicPresburgerarithmetic
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

Branching vector addition systems (BVAS) model how resources can be combined and redistributed along tree-shaped computations. Their reachability problem asks whether a target configuration can arise from given initial configurations by applying a finite set of additive branching rules. The problem had stayed open for decades. This paper shows that non-reachability is always witnessed by a semilinear inductive invariant: a Presburger-definable set that contains the initials, is closed under the rules, and excludes the target. The proof builds such a witness by iteratively growing a single attractor while tracking residual executions outside it with a homogeneous abstract graph of directed runs. When the graph empties, the attractor is already the desired invariant. The result immediately yields a simple decision procedure: enumerate candidate executions in one process and candidate semilinear invariants in another until one succeeds. The same theorem settles the long-open decidability of multiplicative exponential linear logic.

What carries the argument

Safety witnesses (A, W): a semilinear attractor A together with a finite homogeneous set W of directed iruns that cover every initialized run not already inside A. The construction repeatedly extracts a bottom strongly-connected component of W, safely linearizes a portion of its reachable configurations into the attractor, then face-strips the residual difference so that the new directed-irun set is strictly smaller in a well-founded rank.

What would settle it

Exhibit a concrete low-dimensional BVAS together with an unreachable target for which every candidate semilinear set that excludes the target fails to be inductive, or find a counter-example to amalgamation of the embedding order on initialized runs.

Watch

Extended reading notes

Core claim

For every initialized BVAS S and every semilinear set Φ that contains the reachability set of S, there exists a semilinear inductive invariant I for S with I ⊆ Φ. Consequently, if a configuration c is not reachable then $N^d \setminus \{c\}$ contains a semilinear inductive invariant, and BVAS reachability is decidable by parallel enumeration of executions and candidate invariants.

Load-bearing premise

The whole argument rests on the claim that initialized runs ordered by the natural embedding form a well-partial-order that also satisfies amalgamation; if amalgamation fails for some system, the periodic sets attached to runs stop being well-defined and the attractor enlargement collapses.

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 / 4 minor

Summary. The paper proves that BVAS reachability is decidable. The key technical result (Theorem 3.3) states that for every initialized BVAS S and every semilinear set Φ containing Reach(S), there exists a semilinear inductive invariant I for S with I ⊆ Φ. The proof proceeds by iteratively enlarging a semilinear attractor A while maintaining a homogeneous finite set W of directed iruns (pairs (ρ, C) of an initialized run and a finitely-generated cone) that cover all iruns whose targets lie outside A; a well-founded rank on W decreases until W becomes empty, at which point A is the desired invariant. The construction relies on a new safe-linearization lemma for an auxiliary model of well-structured VAS, a face-stripping decomposition of the difference of two finitary cylindric sets, and the wpo+amalgamation property of the embedding order on initialized runs.

Significance. Decidability of BVAS reachability has been open for more than thirty years and is inter-reducible with provability in multiplicative-exponential linear logic; the result therefore settles two long-standing questions at once. The argument supplies a conceptually new forward-only invariant construction that avoids the missing Pre* operator of the classical VAS approach, introduces the notions of attractor and directed irun, and develops the face-stripping theorem and the WSVAS model as reusable geometric tools. Full self-contained proofs of the foundational wpo and amalgamation properties appear in the appendices, so the dependency on prior geometric work is internal and checkable. No complexity upper bound is obtained, but the existence of a simple enumerative decision procedure is already a major advance.

minor comments (4)
  1. The overview at the end of Section 3 is helpful but dense; a short schematic diagram of the two-step update (attractor enlargement then face-stripping of the bottom SCC) would make the global strategy easier to follow on a first reading.
  2. Notation for the various periodic sets (P_ρ, P_w, Q_w, Q_Γ) is introduced gradually; a short table collecting the definitions would reduce the need to flip back and forth.
  3. In the statement of the Face-Stripping Theorem (Theorem 6.1) the phrase “disjoint decomposition” is footnoted; it would be clearer to spell out once that empty sets are allowed.
  4. A few typographical slips remain (e.g., “BV AS” with a space, occasional missing articles). A careful copy-edit pass would polish the presentation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: existence of semilinear inductive invariants is proved by an explicit, terminating forward construction whose supporting geometric and order-theoretic lemmas are either proved in full or imported as independent prior facts.

full rationale

The central claim (Theorem 3.3) is established by iteratively refining safety witnesses (A, W) until W becomes empty, at which point A is the desired semilinear inductive invariant. Each refinement step is justified by three self-contained ingredients proved in the paper: (i) the safe-linearization lemma (Lemma 5.1) obtained by simulating BVAS runs with a well-structured VAS and applying a diamond-map amalgamation argument; (ii) the face-stripping theorem (Theorem 6.1) that decomposes the difference of two finitary Q-cylindric sets along faces of the cone spanned by Q; and (iii) a well-founded rank on finite sets of directed iruns that decreases at every update. The only external geometric facts used are the almost-semilinearity of BVAS reachability sets (imported from the authors’ prior work [3]) and the classical Farkas–Minkowski–Weyl description of cones; both are independent of the existence of inductive invariants and are applied only to guarantee that the periodic sets P_ρ and Q_w are asymptotically definable and finitely generated. The wpo and amalgamation properties of (IRuns(S), ⊴) (Lemma 3.10) are fully re-proved in Appendices B and C by Kruskal’s theorem on decorated trees and by an explicit inductive construction of amalgamating runs; the same amalgamation is re-established for the auxiliary WSVAS model. Consequently no equation, definition or enumeration step reduces the claimed invariant to its own inputs by construction, and the self-citations do not form a load-bearing circular chain.

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

The paper rests on classical well-quasi-order theory, the geometry of periodic sets and cones, and two prior results of the same authors (almost-semilinearity of BVAS reachability sets and the wpo/amalgamation property of iruns). No free parameters appear. The new technical notions (attractors, directed iruns, WSVAS, face stripping) are defined and used only inside the proof; they do not introduce unfalsifiable physical entities.

assumptions (4)
  • standard math Dickson’s lemma / Higman’s lemma / Kruskal’s tree theorem (wqo of N^d, words, trees)
    Used to establish that (IRuns(S), ⊴) and (Runs(V), ⊴) are well-quasi-orders (Lemmas 3.10, 5.2, Appendices B–C).
  • standard math Farkas–Minkowski–Weyl theorem and Farkas lemma for finitely-generated cones
    Invoked to characterize faces of the cone spanned by a full periodic set (Section 6).
  • domain assumption Almost-semilinearity of IBVAS reachability sets (and of the relation S→)
    Cited from the authors’ prior work [3]; used to prove that the periodic sets P_ρ are asymptotically definable (Section 4.2).
  • domain assumption Amalgamation property of the embedding order ⊴ on initialized runs
    Lemma 3.10 (imported from [3]); essential for showing that P_ρ is periodic and that directed iruns behave well under ↠.
invented entities (4)
  • Attractor for an IBVAS
    purpose: A set closed under mixed reachable/attractor leaves; intermediate object that can be enlarged while remaining free of the target.
    Defined in Section 3; used to circumvent the absence of a usable Pre* operator.
  • Directed irun (ρ, C) and the abstract graph G of directed iruns
    purpose: Captures residual executions outside the current attractor while enforcing cone homogeneity inside SCCs.
    Introduced in Section 3; the rank function on finite sets of directed iruns supplies the well-founded measure for termination.
  • Well-structured VAS (WSVAS)
    purpose: Infinite-action extension of VAS that still admits a wqo with amalgamation; used to simulate BVAS runs that have side leaves in the attractor.
    Defined in Section 5.1; safe-linearization lemma proved for it and then transferred back to BVAS.
  • Face-stripping theorem
    purpose: Decomposes the difference of two finitary Q-cylindric sets into a sequence of lower-dimensional cylindric pieces ordered by the reachability relation.
    Theorem 6.1; guarantees that the residual directed-irun set has strictly smaller rank after each enlargement step.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants." pith.science (2026). https://pith.science/paper/WBH5KATL

@misc{pith2026260709558,
  author       = {Pith},
  title        = {Pith review of: Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WBH5KATL}},
  note         = {Machine review of arXiv:2607.09558}
}
read the original abstract

In this paper, we solve the reachability problem for branching vector addition systems (BVAS), a long standing open problem. Our approach is based on semilinear inductive invariants. More precisely, we prove that if a configuration of a BVAS is not reachable, then there exists an inductive invariant, given as a semilinear set, that does not contain this configuration. Based on this property, we deduce a very simple (enumerative) algorithm solving the reachability problem for BVAS.

Figures

Figures reproduced from arXiv: 2607.09558 by the authors.

Figure 1
Figure 1. The runs 𝜌 (left), 𝜎 (middle) and 𝜏 (right) of the BVAS from Example 3.1. 2.3 Linearizations We recall the definition of full1 periodic sets from [16]. A periodic set P ⊆ Z 𝑑 is said to be full if P = G ∩ C for a group G ⊆ Z 𝑑 and a cone C ⊆ Q 𝑑 . Given a periodic set P ⊆ Z 𝑑 , its linearization [27, Section 8] is the full periodic set Lin(P) := (P − P) ∩ Q≥0P. Clearly, a periodic set P is full if, and only if, Lin(… view at source ↗
Figure 2
Figure 2. From left to right : (1) X := (6, 6) + N 2 , (2) Y := {(2, 2), (0, 4)} + N 2 , and (3) 𝑆2 in blue and 𝑆3 in orange. Let Q be a full finitely-generated periodic set, let C := Q≥0Q be the finitely-generated cone spanned by Q, and let F1, . . . , F𝑛 be a linearization of the set of faces of C with respect to ⊇. It follows that 𝑛 = |F (C)|, F (C) = {F1, . . . , F𝑛}, F1 = C, and F𝑖 ⊇ F𝑗 implies 𝑖 ≤ 𝑗. Theorem 6.1 (Face-S… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

41 extracted references · 21 canonical work pages

  1. [1]

    Sergio Abriola, Diego Figueira, and Santiago Figueira. 2017. Logics of Repeating Values on Data Trees and Branching Counter Systems. InFoundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Uppsala, Sweden, April 22-29, 2017 (Lecture Notes in Computer Science, Vol. 10203), Javier Esparza and Andrzej S. Mu...

    work page doi:10.1007/978-3-662-54458-7_12 2017

  2. [2]

    Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre. 2025. On the Reachability Problem for Two- Dimensional Branching VASS. In50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025, August 25-29, 2025, Warsaw, Poland (LIPIcs, Vol. 345), Pawel Gawrychowski, Filip Mazowiecki, and Michal Skrzypczak (Eds.). S...

    work page doi:10.4230/lipics.mfcs.2025.22 2025

  3. [3]

    Clotilde Bizière, Jérôme Leroux, and Grégoire Sutre. 2026. Bridging the Gap Between Plain VASS and Branching VASS. InFoundations of Software Science and Computation Structures - 29th International Conference, FoSSaCS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, P...

    work page doi:10.1007/978-3-032-22730-0_4 2026

  4. [4]

    Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. 2006. Two-variable logic on data trees and XML reasoning. InProceedings of the Twenty-Fifth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 26-28, 2006, Chicago, Illinois, USA, Stijn Vansummeren (Ed.). ACM, 10–19. doi:10.1145/1142351.1142354

    doi:10.1145/1142351.1142354 2006

  5. [5]

    Ahmed Bouajjani and Michael Emmi. 2013. Analysis of Recursively Parallel Programs.ACM Trans. Program. Lang. Syst.35, 3 (2013), 10:1–10:49. doi:10.1145/2518188

    work page doi:10.1145/2518188 2013

  6. [6]

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

    doi:10.1109/lics.2017.8005083 2017

  7. [7]

    Murawski, and C.-H

    Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. 2017. ML and Extended Branching VASS. In 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 (Lecture Notes in Comp...

    work page doi:10.1007/978-3-662-54434- 2017

  8. [8]

    Wojciech Czerwiński and Łukasz Orlikowski. 2022. Reachability in Vector Addition Systems is Ackermann-complete. In2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). 1229–1240. doi:10.1109/FOCS52979. 2021.00120

    doi:10.1109/focs52979 2022

Show all 41 references
  1. [9]

    Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. 2004. Vector Addition Tree Automata. In19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. IEEE Computer Society, 64–73. doi:10.1109/LICS.2004.1319601

    2004 doi arXiv

  2. [10]

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

    2013 doi

  3. [11]

    Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. 2017. Polynomial-Space Complete- ness of Reachability for Succinct Branching VASS in Dimension One. In44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14...

    2017 doi

  4. [12]

    Ginsburg and E

    S. Ginsburg and E. H. Spanier. 1966. Semigroups, Presburger Formulas, and Languages.Pacific J. Math.16, 2 (1966), 285–296. doi:10.2140/pjm.1966.16.285

    1966 doi

  5. [13]

    Stefan Göller, Christoph Haase, Ranko Lazić, and Patrick Totzke. 2016. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. InICALP (LIPIcs, Vol. 55). Schloss Dagstuhl, 105:1–105:13. doi:10.4230/LIPIcs. ICALP.2016.105

    2016 doi

  6. [14]

    Roland Guttenberg, Wojciech Czerwiński, and Sławomir Lasota. 2025. Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests. In2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 581–593. doi:10.1109/LICS65433.2025.00050

    2025 doi

  7. [15]

    Roland Guttenberg, Eren Keskin, and Roland Meyer. 2025. PVASS Reachability is Decidable. to appear at LICS 2026. arXiv:arXiv:2504.05015

    2025

  8. [16]

    Raskin, and Javier Esparza

    Roland Guttenberg, Mikhail A. Raskin, and Javier Esparza. 2023. Geometry of Reachability Sets of Vector Addition Systems. In34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium, September 18-23, 2023 (LIPIcs), Guillermo A. Pérez and Jean-François ...

    2023 doi

  9. [17]

    Florent Jacquemard, Luc Segoufin, and Jérémie Dimino. 2016. FO2(<,+1, ) on data trees, data tree automata and branching vector addition systems.Logical Methods in Computer Science12, 2 (2016), 32. doi:10.2168/LMCS-12(2:3)2016 Solving the Reachability Problem for Branching Vect...

    2016 doi

  10. [18]

    Petr Jancar. 1990. Decidability of a Temporal Logic Problem for Petri Nets.Theor. Comput. Sci.74, 1 (1990), 71–93. doi:10.1016/0304-3975(90)90006-4

    1990 doi

  11. [19]

    Łukasz Kamiński and Sławomir Lasota. 2024. Bi-Reachability in Petri Nets with Data. In35th International Conference on Concurrency Theory (CONCUR 2024) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 311), Rupak Majumdar and Alexandra Silva (Eds.). Schloss Dag...

    2024 doi

  12. [20]

    Łukasz Kamiński and Sławomir Lasota. 2025. Reachability in Symmetric VASS. In50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 345), Paweł Gawrychowski, Filip Mazowiecki, an...

    2025 doi

  13. [21]

    Kanovich

    Max I. Kanovich. 1995. Petri Nets, Horn Programs, Linear Logic and Vector Games.Ann. Pure Appl. Log.75 (1995), 107–135. https://api.semanticscholar.org/CorpusID:14642978

    1995

  14. [22]

    Rao Kosaraju

    S. Rao Kosaraju. 1982. Decidability of reachability in vector addition systems (Preliminary Version). InProceedings of the Fourteenth Annual ACM Symposium on Theory of Computing(San Francisco, California, USA)(STOC ’82). Association for Computing Machinery, New York, NY, USA, ...

    1982 doi

  15. [23]

    J.L. Lambert. 1992. A structure to decide reachability in Petri nets.Theoretical Computer Science99, 1 (1992), 79–104. doi:10.1016/0304-3975(92)90173-D

    1992 doi

  16. [24]

    Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. 2008. Nets with Tokens which Carry Data.Fundam. Informaticae88, 3 (2008), 251–274. http://content.iospress.com/articles/fundamenta- informaticae/fi88-3-03

    2008

  17. [25]

    Ranko Lazić and Sylvain Schmitz. 2015. Nonelementary Complexities for Branching VASS, MELL, and Extensions. ACM Trans. Comput. Log.16, 3 (2015), 20:1–20:30. doi:10.1145/2733375

    2015 doi

  18. [26]

    Jérôme Leroux. 2011. Vector addition system reachability problem: a short self-contained proof. InProceedings of POPL

    2011

  19. [27]

    Jerome Leroux. 2012. Vector Addition Systems Reachability Problem (A Simpler Solution). InTuring-100. The Alan Turing Centenary (EPiC Series in Computing, Vol. 10), Andrei Voronkov (Ed.). EasyChair, 214–228. doi:10.29007/bnx2

    2012 doi

  20. [28]

    Jérôme Leroux. 2021. The Reachability Problem for Petri Nets is Not Primitive Recursive. In62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022. IEEE, 1241–1252. doi:10.1109/FOCS52979.2021.00121

    2021 doi

  21. [29]

    Jerome Leroux and Sylvain Schmitz. 2015. Demystifying Reachability in Vector Addition Systems. InProceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (LICS ’15). IEEE Computer Society, USA, 56–67. doi:10.1109/LICS.2015.16

    2015 doi

  22. [30]

    Jérôme Leroux and Sylvain Schmitz. 2019. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. IEEE, 1–13. doi:10.1109/LICS.2019.8785796

    2019 doi

  23. [31]

    Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar. 1992. Decision problems for propositional linear logic.Annals of Pure and Applied Logic56, 1 (1992), 239–311. doi:10.1016/0168-0072(92)90075-B

    1992 doi

  24. [32]

    Rupak Majumdar and Zilong Wang. 2013. Expand, Enlarge, and Check for Branching Vector Addition Systems. In CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings (Lecture Notes in Computer Science...

    2013 doi

  25. [33]

    Ernst W. Mayr. 1984. An Algorithm for the General Petri Net Reachability Problem.SIAM J. Comput.13, 3 (1984), 441–460. doi:10.1137/0213029

    1984 doi

  26. [34]

    Filip Mazowiecki and Michal Pilipczuk. 2019. Reachability for Bounded Branching VASS. In30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, The Netherlands, August 27-30, 2019 (LIPIcs, Vol. 140), Wan J. Fokkink and Rob van Glabbeek (Eds.). Schloss Dags...

    2019

  27. [35]

    Owen Rambow. 1994. Multiset-Valued Linear Index Grammars: Imposing Dominance Constraints on Derivations. In 32nd Annual Meeting of the Association for Computational Linguistics, 27-30 June 1994, New Mexico State University, Las Cruces, New Mexico, USA, Proceedings, James Puste...

    1994 doi

  28. [36]

    Klaus Reinhardt. 2008. Reachability in Petri Nets with Inhibitor Arcs.Electronic Notes in Theoretical Computer Science 223 (2008), 239–264. Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008). doi:10.1016/j.entcs.2008.12.042

    2008 doi

  29. [37]

    Sylvain Schmitz and Philippe Schnoebelen. 2012. Algorithmic Aspects of WQO Theory. (Aug. 2012). Lecture. https://cel.hal.science/cel-00727025

    2012

  30. [38]

    1999.Theory of linear and integer programming

    Alexander Schrijver. 1999.Theory of linear and integer programming. Wiley. 28 Clotilde Bizière, Jérôme Leroux, and Grégoire Sutre

    1999

  31. [39]

    Wim Veldman and Marc Bezem. 1993. Ramsey’s Theorem and the Pigeonhole Principle in Intuitionistic Mathematics. Journal of the London Mathematical Societys2-47, 2 (1993), 193–211. doi:10.1112/jlms/s2-47.2.193

    1993 doi

  32. [40]

    decorated

    Kumar Neeraj Verma and Jean Goubault-Larrecq. 2005. Karp-Miller Trees for a Branching Extension of VASS.Discret. Math. Theor. Comput. Sci.7, 1 (2005), 217–230. doi:10.46298/DMTCS.350 Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductiv...

    2005 doi

  33. [41]

    Moreover, we have src(𝜎)= f0 =src(𝛼 0) +src(𝛽 0) − c0 =src(𝛼) +src(𝛽) −src(𝜌) and tgt(𝜎)= h𝑘 =tgt(𝛼 𝑘 ) +tgt(𝛽 𝑘 ) − c𝑘 =tgt(𝛼) +tgt(𝛽) −tgt(𝜌)

    · · ·𝑤𝑘 (𝜎𝑘 ★𝜎 ′ 𝑘 ) is a run. Moreover, we have src(𝜎)= f0 =src(𝛼 0) +src(𝛽 0) − c0 =src(𝛼) +src(𝛽) −src(𝜌) and tgt(𝜎)= h𝑘 =tgt(𝛼 𝑘 ) +tgt(𝛽 𝑘 ) − c𝑘 =tgt(𝛼) +tgt(𝛽) −tgt(𝜌) . This entails that dir(𝜌) +dir(𝜎)= dir(𝛼) +dir(𝛽). It remains to show that𝛼, 𝛽⊴𝜎. We will use Corolla...

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.