pith. sign in

arxiv: 2606.30042 · v1 · pith:RPM474X7new · submitted 2026-06-29 · 💻 cs.FL · cs.CC· cs.LO

Reachability in Fixed-Dimensional Continuous VASS

Michal Ajdar\'ow , A. R. Balasubramanian , {\L}ukasz Orlikowski This is my paper

Pith reviewed 2026-06-30 03:42 UTC · model grok-4.3

classification 💻 cs.FL cs.CCcs.LO
keywords continuous VASSreachabilitycoverabilityfixed dimensionNP-completenessAC1Egyptian fractions
0
0 comments X

The pith

Continuous VASS reachability and coverability are in AC1 for one counter but NP-complete for two or more counters.

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

The paper classifies the complexity of eight variants of reachability and coverability for continuous VASS, where counters hold non-negative rationals and each added vector is scaled by an arbitrary rational factor in (0,1]. With a single counter, every variant belongs to the parallel complexity class AC1. With two or more counters, every variant is NP-complete, and the hardness result continues to hold when the underlying automaton is acyclic. The classification is obtained via a new reduction method called the Egyptian prime fractions technique that maps known hard problems onto CVASS instances while keeping the continuous scaling rules intact. The same split appears for integer transition vectors except at dimension two, which is left open.

Core claim

For rational transition vectors, all eight problems are in AC¹ when the dimension is 1 and NP-complete when the dimension is at least 2; the NP-hardness holds even for acyclic automata. The proof introduces the Egyptian prime fractions technique. For integer vectors the same split holds except that dimension two remains unclassified.

What carries the argument

The Egyptian prime fractions technique, which reduces known NP-hard problems to fixed-dimensional CVASS reachability and coverability instances while preserving the continuous rational scaling semantics.

If this is right

  • One-dimensional CVASS reachability can be decided by constant-depth polynomial-size circuits.
  • Two-dimensional CVASS reachability remains NP-complete even when the control automaton contains no cycles.
  • The NP-completeness classification applies uniformly to reachability, coverability, unary and binary encodings, and both non-negative and rational semantics.
  • For integer transition vectors the problems become NP-complete from dimension three onward.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The open status of dimension two with integer vectors may require a separate analysis that does not rely on the prime-fraction construction.
  • The AC1 membership for one dimension suggests that one-counter continuous systems admit efficient parallel decision procedures.
  • The reduction technique could be tested on other relaxed counter models to locate similar dimension thresholds.

Load-bearing premise

The Egyptian prime fractions technique correctly reduces known NP-hard problems to CVASS instances while preserving the continuous rational scaling semantics.

What would settle it

A concrete two-dimensional CVASS instance whose reachability answer contradicts the answer produced by applying the Egyptian prime fractions reduction from a known NP-complete problem.

read the original abstract

Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is Ackermann-complete. Because of this huge complexity, various over-approximations of VASS have been studied in the literature. One such over-approximation is continuous VASS (CVASS), in which the counters are (non-negative) rational numbers and whenever a vector is added to the current counter values, it is first scaled with an arbitrarily chosen rational factor between zero and one. It is known that the reachability problem for CVASS is $\mathsf{NP}$-complete. In this paper, we initiate the study of fixed-dimensional CVASS, i.e., CVASS with a fixed number of counters. We study both the reachability and coverability problems, under both unary and binary encodings as well as over both the non-negative and the rational semantics. This gives rise to a collection of eight different problems. As our main result, we prove a complexity dichotomy for all of these eight problems when the transition vectors are over the rationals: For dimension 1, all of the eight problems are in $\mathsf{AC}^1$, whereas for any dimension at least 2, all of the eight problems are $\mathsf{NP}$-complete. Furthermore, the hardness holds even when the underlying automaton is acyclic. To achieve this result, we present a new technique called the Egyptian prime fractions technique. Finally, we also study these problems when the transition vectors are over the integers. Except for dimension 2, we classify the complexity of these problems over the non-negative semantics: For dimension 1, all of the problems are in $\mathsf{AC}^1$, whereas for dimensions 3 and above, all of the problems are $\mathsf{NP}$-complete.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper claims a complexity dichotomy for the eight variants of reachability and coverability in fixed-dimensional continuous VASS (CVASS) with rational transition vectors: all are in AC^1 for dimension 1, and all are NP-complete for any dimension >=2 (even when the automaton is acyclic). Hardness is obtained via a new Egyptian prime fractions technique. For integer transition vectors under non-negative semantics, the problems are in AC^1 for dimension 1 and NP-complete for dimensions >=3 (dimension 2 left open).

Significance. If the Egyptian prime fractions reductions are correct, the result supplies a sharp, uniform classification separating dimension 1 from all higher fixed dimensions for both reachability and coverability under continuous semantics. This is significant because it shows that the continuous over-approximation does not drop below NP-completeness once dimension reaches 2, and that hardness survives acyclicity. The new technique is explicitly credited as the vehicle for preserving rational scaling in the reductions.

major comments (1)
  1. [Abstract and Egyptian prime fractions technique section] Abstract and the section presenting the Egyptian prime fractions technique: the NP-completeness claim for all eight problems when dimension >=2 rests entirely on the new reduction technique correctly mapping an NP-hard source problem to a fixed-dimension CVASS instance while preserving (i) exact correspondence between rational scaling factors in [0,1] and choices in the source instance, (ii) acyclicity of the target when the source is acyclic, and (iii) absence of extraneous solutions introduced by the continuous non-negative/rational semantics. No equations, lemmas, or verification of these three preservation properties appear in the supplied text, rendering the central hardness claim unverifiable.
minor comments (1)
  1. The integer-vector case leaves dimension 2 open; a brief statement of the partial results or obstacles for that single case would improve completeness.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need for greater detail in the presentation of our main technical contribution. We agree that the current text does not supply sufficient verification of the reduction properties and will revise the manuscript to address this.

read point-by-point responses

  1. Referee: [Abstract and Egyptian prime fractions technique section] Abstract and the section presenting the Egyptian prime fractions technique: the NP-completeness claim for all eight problems when dimension >=2 rests entirely on the new reduction technique correctly mapping an NP-hard source problem to a fixed-dimension CVASS instance while preserving (i) exact correspondence between rational scaling factors in [0,1] and choices in the source instance, (ii) acyclicity of the target when the source is acyclic, and (iii) absence of extraneous solutions introduced by the continuous non-negative/rational semantics. No equations, lemmas, or verification of these three preservation properties appear in the supplied text, rendering the central hardness claim unverifiable.

    Authors: We acknowledge that the submitted manuscript does not contain explicit lemmas or equations verifying the three preservation properties listed by the referee. This is a substantive gap that prevents independent verification of the hardness results from the text. In the revised version we will expand the Egyptian prime fractions technique section with (a) a formal definition of the reduction, (b) lemmas establishing that rational scaling factors in [0,1] correspond exactly to choices in the source instance, (c) a proof that acyclicity is preserved, and (d) an argument that the continuous semantics introduce no extraneous solutions. These additions will make the NP-completeness claims for dimension >=2 fully verifiable while leaving the AC^1 membership results for dimension 1 unchanged. revision: yes

Circularity Check

0 steps flagged

No circularity; results from new reductions and direct analysis

full rationale

The paper establishes the complexity dichotomy via a newly introduced Egyptian prime fractions technique for many-one reductions establishing NP-hardness (dimensions >=2, even acyclic) together with separate membership arguments placing all eight problems in AC^1 for dimension 1. No quoted step equates a claimed result to its own inputs by definition, renames a fitted parameter as a prediction, or loads the central claim on a self-citation chain. The derivation is self-contained against external benchmarks (standard NP-hardness sources and AC^1 algorithms) and does not presuppose the target classification.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard definitions and known NP-completeness of unrestricted CVASS reachability; no fitted numerical parameters or new postulated entities are introduced.

axioms (1)
  • domain assumption Standard definitions of VASS, CVASS, reachability, coverability, and complexity classes AC^1 and NP.
    The dichotomy is stated relative to these background notions from automata and complexity theory.

pith-pipeline@v0.9.1-grok · 5893 in / 1280 out tokens · 52343 ms · 2026-06-30T03:42:15.054264+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

15 extracted references · 9 canonical work pages

  1. [1]

    1 A. R. Balasubramanian. Parameterized complexity of safety of threshold automata. In Nitin Saxena and Sunil Simon, editors,40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference), December 14-18, 2020, LIPIcs, pages 37:1–37:15. Sch...

    2020

  2. [2]

    URL:https: //doi.org/10.4230/LIPIcs.FSTTCS.2020.37,doi:10.4230/LIPICS.FSTTCS.2020.37. 2 A. R. Balasubramanian, Javier Esparza, and Mikhail A. Raskin. Finding cut-offs in leaderless rendez-vous protocols is easy.Log. Methods Comput. Sci., 19(4),

    work page doi:10.4230/lipics.fsttcs.2020.37 2020

  3. [3]

    org/10.46298/lmcs-19(4:2)2023,doi:10.46298/LMCS-19(4:2)2023

    URL:https://doi. org/10.46298/lmcs-19(4:2)2023,doi:10.46298/LMCS-19(4:2)2023. 3 Pascal Baumann, Flavio D’Alessandro, Moses Ganardi, Oscar H. Ibarra, Ian McQuillan, Lia Schütze, and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters. In Orna Kupferman and Pawel Sobocinski, editors,Foundations of Software Science and Computat...

    work page doi:10.46298/lmcs-19(4:2)2023 2023

  4. [4]

    153,doi:10.4230/LIPICS.ICALP.2025.153

    URL:https://doi.org/10.4230/LIPIcs.ICALP.2025. 153,doi:10.4230/LIPICS.ICALP.2025.153. 10 Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229–1240. IEEE, 2021.doi: 10.1109/FOCS529...

    work page doi:10.4230/lipics.icalp.2025 2025

  5. [5]

    12 Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

    doi:10.1007/978-3-642-10669-9. 12 Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of popu- lation protocols.Acta Informatica, 54(2):191–215,

    work page doi:10.1007/978-3-642-10669-9

  6. [6]

    13 Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J

    URL:https://doi.org/10.1007/ s00236-016-0272-3,doi:10.1007/S00236-016-0272-3. 13 Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic. An SMT-based approach to coverability analysis. In Armin Biere and Roderick Bloem, editors,Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vien...

    work page doi:10.1007/s00236-016-0272-3 2014

  7. [7]

    Cavada, A

    Proceedings, Lecture Notes in Computer Science, pages 603–619. Springer, 2014.doi: 10.1007/978-3-319-08867-9\_40. 14 Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes.J. ACM, 39(3):675–735, 1992.doi:10.1145/146637.146681. 15 Eitan M. Gurari and Oscar H. Ibarra. The complexity of the equivalence problem for simple programs....

    work page doi:10.1007/978-3-319-08867-9 2014

  8. [8]

    17 Monika Heiner, David R

    doi:10.1007/978-3-032-01436-8\_6. 17 Monika Heiner, David R. Gilbert, and Robin Donaldson. Petri nets for systems and synthetic biology. In Marco Bernardo, Pierpaolo Degano, and Gianluigi Zavattaro, editors,Formal Methods for Computational Systems Biology, 8th International School on Formal Methods for the Design of Computer, Communication, and Software S...

    work page doi:10.1007/978-3-032-01436-8 2008

  9. [9]

    20 Jérôme Leroux

    doi:10.1016/S0022-0000(02)00025-9. 20 Jérôme Leroux. 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, pages 1241–1252. IEEE, 2021.doi:10.1109/FOCS52979.2021.00121. 21 C. Mahulea, L. Recalde, and M. Silva. On performance mono...

    work page doi:10.1016/s0022-0000(02)00025-9 2021

  10. [10]

    1984 , issn =

    URL:https://www.sciencedirect.com/science/article/pii/ 0166218X84900817,doi:10.1016/0166-218X(84)90081-7. 26 Wil M. P. van der Aalst. The application of Petri nets to workflow management.J. Circuits Syst. Comput., 8(1):21–66, 1998.doi:10.1142/S0218126698000043. 27 Heribert Vollmer.Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoret- ...

    work page doi:10.1016/0166-218x(84)90081-7 1998

  11. [11]

    Subcase 2: xi < xj

    Hence, this indeed gives a run frompi(xi) top j(xj)where all the intermediate counter values lie in[x−ϵ,y+ϵ]. Subcase 2: xi < xj. By assumption, we have∆ := xj−xi = ∑ tk∈T+∪T−αkwk. Let W+ := ∑ tk∈T+αkwk and W−:= ∑ tk∈T−αk|wk|. Note thatW+ = ∆ + W−. We shall now modify the run so that each negative and neutral transitiontk is now fired by the fraction αk/N...

    2026

  12. [12]

    We then let δ:=v−u+ϵwithm =⌈δ⌉

    If W−(C) = 0, then we letϵ= 0; otherwise, we letϵ∈(0, 1]such that ϵ≤W−(C). We then let δ:=v−u+ϵwithm =⌈δ⌉. We now fire eachti with a fractionαi as follows: Ifwi≥0, then we setαi := δ mW+(C); otherwise, we setαi := ϵ mW−(C). By construction, it is seen that this is a Q-run fromr(u)to r(u + ∆)where∆ = ∑ wi>0 v−u+ϵ mW+(C)·wi−∑ wi<0 ϵ mW−(C)·|wi|= v−u+ϵ m −ϵ ...

    2026

  13. [13]

    Since G′can be constructed fromGM in logarithmic space and sinceL⊆NL⊆AC1, it follows that we have anAC1 algorithm in this case

    This latter problem is known to be inAC1 [24, Theorem III.2]. Since G′can be constructed fromGM in logarithmic space and sinceL⊆NL⊆AC1, it follows that we have anAC1 algorithm in this case. Finally, suppose the update vectors are rational numbers. We show that we can reduce this case to the previous case of integer update vectors over the binary encoding....

    2026

  14. [14]

    ∗ − →Q+ b1(g1,h 1)... ∗ − →Q+ bm(gm,hm) :=b m(1,0) CONCUR 2026 41:26 Reachability in Fixed-Dimensional Continuous VASS Repeated applications of Proposition 25 imply that, for each1≤i≤m, there is a number ji which is the product of some non-empty subset of{P(ℓ1 i ),P (ℓ2 i ),P (ℓ3 i )}such that gi = ji·gi−1This implies that,gm := 1 = g0·∏ 1≤i≤mji = f(A)·∏ ...

    2026

  15. [15]

    CONCUR 2026 41:28 Reachability in Fixed-Dimensional Continuous VASS Proof.By construction ofM ′there is aQ+-run inMof the form a0(1,0) :=a 0(g0,h

    ) coveringb′ m(0,1,L)inM ′. CONCUR 2026 41:28 Reachability in Fixed-Dimensional Continuous VASS Proof.By construction ofM ′there is aQ+-run inMof the form a0(1,0) :=a 0(g0,h

    2026