pith. sign in

arxiv: 1907.11010 · v1 · pith:RWADVVHHnew · submitted 2019-07-25 · 💻 cs.FL · cs.CC

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Tom\'a\v{s} Br\'azdil , Krishnendu Chatterjee , Anton\'in Ku\v{c}era , Petr Novotn\'y , Dominik Velan This is my paper

Pith reviewed 2026-05-24 15:50 UTC · model grok-4.3

classification 💻 cs.FL cs.CC
keywords probabilistic VASSnondeterminismexpected termination timedecidabilitypolynomial timeasymptotic analysisvector addition systemsMarkov processes
0
0 comments X

The pith

For a natural class of probabilistic VASS with nondeterminism, deciding whether asymptotic expected termination time is linear can be done in polynomial time, and non-linear cases are at least quadratic.

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

The paper examines probabilistic vector addition systems with states that incorporate nondeterminism to abstract probabilistic programs. It focuses on the worst expected number of transitions to termination from an initial configuration of size n. Techniques are developed to decide if this expected time grows linearly with n, and the decision runs in polynomial time for a certain natural class of such systems. The work also proves a dichotomy: when the time is not linear it is necessarily at least quadratic. These results matter for verifying runtime behavior in models of probabilistic computation.

Core claim

The paper claims that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. It further shows that if the asymptotic expected termination time is not linear then it is at least quadratic, i.e., in Ω(n²).

What carries the argument

Polynomial-time decision procedure for linearity of worst-case expected termination time together with the linear-versus-quadratic dichotomy for pVASS with nondeterminism.

If this is right

  • The expected termination time of systems in the class exhibits a strict linear-or-quadratic dichotomy.
  • Fast termination can be verified algorithmically in polynomial time for the class.
  • pVASS abstractions of probabilistic programs can be checked for linear expected runtime bounds.
  • Non-linear cases automatically satisfy a quadratic lower bound on expected steps.

Where Pith is reading between the lines

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

  • The decision procedure may serve as a building block for automated tools that certify expected runtime of probabilistic programs.
  • Similar linearity checks could be investigated for related models such as probabilistic pushdown automata.
  • The dichotomy suggests that intermediate growth rates are impossible under the syntactic or semantic restrictions defining the class.

Load-bearing premise

A certain natural class of pVASS with nondeterminism exists on which the polynomial-time decision procedure for linear expected termination time applies.

What would settle it

An instance belonging to the natural class whose measured expected termination time grows strictly between linear and quadratic, such as Θ(n log n), would refute the dichotomy.

Figures

Figures reproduced from arXiv: 1907.11010 by Anton\'in Ku\v{c}era, Dominik Velan, Krishnendu Chatterjee, Petr Novotn\'y, Tom\'a\v{s} Br\'azdil.

Figure 1
Figure 1. Figure 1: VASS MDP A1 (left) and A2 (right). The states p1, p2 are probabilistic, and the states q1, q2 are nondeterministic. 3 Linearity of Demonic Termination Time In this paper, we prove the following theorem: Theorem 1. The problem whether the expected termination time of a given strongly connected VASS MDP A is linear is decidable in polynomial time. If the expected termination time of A is not linear, then Ld(… view at source ↗
Figure 2
Figure 2. Figure 2: A trajectory for the scheme of Example 2. p1 r p2 (0,0) (0,0) 1 4 ,(0,0) f 3 4 ,(0,0) (2, −1) (−1, 2) (0, −1) [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
read the original abstract

A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in $\Omega(n^2)$.

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

0 major / 3 minor

Summary. The manuscript develops techniques for checking fast termination of probabilistic vector addition systems with states (pVASS) that include nondeterminism. For a certain natural class of such pVASS (defined syntactically in Section 3), it shows that whether the asymptotic expected termination time is linear (O(n)) is decidable in polynomial time via reduction to a graph-theoretic condition on the underlying VASS. It further proves a dichotomy: if the expected termination time is not linear, then it is necessarily at least quadratic (Ω(n²)), established via a separate pumping argument that excludes intermediate growth rates.

Significance. If the result holds, it provides an efficient (P-time) decision procedure for a practically relevant termination property in a subclass of pVASS, which serve as abstractions for probabilistic programs. The combination of polynomial-time decidability with a clean linear-vs-quadratic dichotomy strengthens the contribution, as does the explicit reduction to graph reachability and the pumping argument ruling out other growth rates. These features make the work a solid addition to the literature on verification of infinite-state probabilistic systems.

minor comments (3)
  1. [§2] §2: The definition of configurations and the blocking semantics for counter decrements below zero could be illustrated with a small concrete example to aid readability for readers new to VASS.
  2. [§4] §4: The statement of the main theorem (presumably Theorem 1 or 2) would benefit from an explicit reference back to the syntactic restrictions of the natural class introduced in §3.
  3. The paper would be strengthened by a brief discussion (even if informal) of how the natural class relates to common syntactic restrictions appearing in the probabilistic-program literature.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive evaluation of the manuscript and for recommending acceptance. The report accurately captures the main contributions regarding the polynomial-time decidability result and the linear-vs-quadratic dichotomy for asymptotic expected termination time in the considered class of nondeterministic pVASS.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central result is a polynomial-time decision procedure for linearity of expected termination time in a syntactically restricted subclass of pVASS with nondeterminism, obtained by reduction to a graph-theoretic condition on the underlying VASS plus a separate pumping argument establishing the linear-vs-quadratic dichotomy. No load-bearing step is shown to reduce by the paper's own equations or self-citation to a fitted input, self-definition, or prior result by the same authors; the argument is presented as resting on external combinatorial techniques rather than internal fitting or renaming.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on an unspecified 'natural class' of models and on standard background results in automata theory and Markov decision processes. No free parameters or invented entities are visible from the abstract.

axioms (1)
  • standard math Standard results on decidability and complexity for vector addition systems and Markov decision processes hold.
    Invoked implicitly when claiming polynomial-time decidability.

pith-pipeline@v0.9.0 · 5738 in / 1209 out tokens · 14716 ms · 2026-05-24T15:50:36.724307+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

50 extracted references · 50 canonical work pages

  1. [1]

    de Alfaro, L.: Formal verification of probabilistic syste ms. Phd. thesis, Stanford University, Stanford, CA, USA (1998)

    work page 1998

  2. [2]

    In: Proceedings of ICALP 2015

    Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness o f parameterized timed networks. In: Proceedings of ICALP 2015. pp. 375–387 (2015)

    work page 2015

  3. [3]

    International Journal of Foundations of Computer Science 22(04), 783–799 (2011)

    Atig, M.F., Habermehl, P.: On yen’s path logic for petri ne ts. International Journal of Foundations of Computer Science 22(04), 783–799 (2011)

    work page 2011

  4. [4]

    Baier, C., Katoen, J.P.: Principles of Model Checking (20 08)

    work page

  5. [5]

    In: Proceedings of LI CS’16

    Barthe, G., Gaboardi, M., Gr´ egoire, B., Hsu, J., Strub, P .Y.: Proving differential privacy via probabilistic couplings. In: Proceedings of LI CS’16. pp. 749–758. ACM, New York, NY, USA (2016) Deciding Fast Termination for Probabilistic V ASS 15

    work page 2016

  6. [6]

    , Veith, H., Widder, J.: Decidability in parameterized verification

    Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S. , Veith, H., Widder, J.: Decidability in parameterized verification. SIGACT News 47(2), 53–64 (2016)

    work page 2016

  7. [7]

    In: Proceedings of RP 2011

    Bozzelli, L., Ganty, P.: Complexity analysis of the backw ard coverability algorithm for vass. In: Proceedings of RP 2011. pp. 96–109 (2011)

    work page 2011

  8. [8]

    Br´ azdil, T., Broˇ zek, V., Chatterjee, K., Forejt, V., Ku ˇ cera, A.: Markov decision processes with multiple long-run average objectives 10(1), 1–29 (2014)

    work page 2014

  9. [9]

    In: Proceed ings of ICALP 2011, Part II

    Br´ azdil, T., Broˇ zek, V., Etessami, K., Kuˇ cera, A.: Approximating the termination value of one-counter MDPs and stochastic games. In: Proceed ings of ICALP 2011, Part II. vol. 6756, pp. 332–343 (2011)

    work page 2011

  10. [10]

    In: Proceed- ings of LICS 2018

    Br´ azdil, T., Chatterjee, K., Kuˇ cera, A., Novotn´ y, P., Velan, D., Zuleger, F.: Effi- cient algorithms for asymptotic bounds on termination time in V ASS. In: Proceed- ings of LICS 2018. pp. 185–194 (2018)

    work page 2018

  11. [11]

    Br´ azdil, T., Kiefer, S., Kuˇ cera, A.: Efficient analysisof probabilistic programs with an unbounded counter. J. ACM 61(6) (2014)

    work page 2014

  12. [12]

    In: P roceedings of ICALP 2012, Part II

    Br´ azdil, T., Kuˇ cera, A., Novotn´ y, P., Wojtczak, D.: Minimizing expected termi- nation time in one-counter Markov decision processes. In: P roceedings of ICALP 2012, Part II. vol. 7392, pp. 141–152 (2012)

    work page 2012

  13. [13]

    In: 2011 Eleventh International Conference on Appl ication of Concurrency to System Design

    Cassez, F.: Timed games for computing WCET for pipelined processors with caches. In: 2011 Eleventh International Conference on Appl ication of Concurrency to System Design. pp. 195–204 (June 2011)

    work page 2011

  14. [14]

    In: Proceedings of FSTTCS 2010

    Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.F .: Generalized mean-payoff and energy games. In: Proceedings of FSTTCS 2010. pp. 505–51 6 (2010)

    work page 2010

  15. [15]

    In: Proceedings of CONCUR 2013

    Chatterjee, K., Velner, Y.: Hyperplane separation tech nique for multidimensional mean-payoff games. In: Proceedings of CONCUR 2013. pp. 500–5 15 (2013)

    work page 2013

  16. [16]

    In: CA V (2017)

    Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomi al worst-case analysis of recursive programs. In: CA V (2017)

    work page 2017

  17. [17]

    In: Computer Aided Verific ation

    Chatterjee, K., Fu, H., Murhekar, A.: Automated recurre nce analysis for almost- linear expected-runtime bounds. In: Computer Aided Verific ation. Springer Inter- national Publishing (2017)

    work page 2017

  18. [18]

    In: Proceedings of LICS 2017

    Colcombet, T., Jurdzinski, M., Lazic, R., Schmitz, S.: P erfect half space games. In: Proceedings of LICS 2017. pp. 1–11 (2017)

    work page 2017

  19. [19]

    In: Proceedings of STOC 2019

    Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazow iecki, F.: The reachability problem for petri nets is not elementary. In: Proceedings of STOC 2019. pp. 24–33 (2019)

    work page 2019

  20. [20]

    Lectures on Petri nets I: Basic models pp

    Esparza, J.: Decidability and complexity of petri net pr oblems – an introduction. Lectures on Petri nets I: Basic models pp. 374–428 (1998)

    work page 1998

  21. [21]

    Esparza, J., Kuˇ cera, A., Mayr, R.: Model-checking prob abilistic pushdown au- tomata 2(1:2), 1–31 (2006)

    work page 2006

  22. [22]

    , Niksic, F.: An smt- based approach to coverability analysis

    Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P. , Niksic, F.: An smt- based approach to coverability analysis. In: Proceedings o f CA V 2014. pp. 603–619 (2014)

    work page 2014

  23. [23]

    Bulletin of the EATCS 52, 245–262 (1994)

    Esparza, J., Nielsen, M.: Decidability issues for petri nets – a survey. Bulletin of the EATCS 52, 245–262 (1994)

    work page 1994

  24. [24]

    Etessami, K., Yannakakis, M.: Model checking of recursi ve probabilistic systems 13 (2012)

    work page 2012

  25. [25]

    In: Thiemann, P

    Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silv a, A.: Probabilistic netkat. In: Thiemann, P. (ed.) European Symposium on Programming. L NCS, vol. 9632, pp. 282–309. Springer Berlin Heidelberg, Berlin, Heidelbe rg (2016)

    work page 2016

  26. [26]

    Nature 521(7553), 452–459 (2015) 16 T

    Ghahramani, Z.: Probabilistic machine learning and art ificial intelligence. Nature 521(7553), 452–459 (2015) 16 T. Br´ azdil et al

    work page 2015

  27. [27]

    In: Proceedin gs of POPL’09

    Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: Precise a nd efficient static esti- mation of program computational complexity. In: Proceedin gs of POPL’09. pp. 127–139. ACM, New York, NY, USA (2009)

    work page 2009

  28. [28]

    ACM Trans

    Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amor tized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1–14:62 (2012)

    work page 2012

  29. [29]

    In: Proceedings of ICALP 2015

    Jurdzinski, M., Lazic, R., Schmitz, S.: Fixed-dimensio nal energy games are in pseudo-polynomial time. In: Proceedings of ICALP 2015. pp. 260–272 (2015)

    work page 2015

  30. [30]

    Acta Inf

    Kaminski, B.L., Katoen, J., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Inf. 56(3), 255–285 (2019)

    work page 2019

  31. [31]

    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Wea kest precondition rea- soning for expected runtimes of randomized algorithms. J. A CM 65(5), 30:1–30:68 (2018)

    work page 2018

  32. [32]

    Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)

    work page 1969

  33. [33]

    In: Proceedings of STOC 1982

    Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of STOC 1982. pp. 267–281. ACM (19 82)

    work page 1982

  34. [34]

    In: Proceedings of STOC 1988

    Kosaraju, S.R., Sullivan, G.F.: Detecting cycles in dyn amic graphs in polynomial time. In: Proceedings of STOC 1988. pp. 398–406 (1988)

    work page 1988

  35. [35]

    In: Proceedings of POPL 2011

    Leroux, J.: Vector addition system reachability proble m: A short self-contained proof. In: Proceedings of POPL 2011. pp. 307–316 (2011)

    work page 2011

  36. [36]

    In: Proceedings of ICALP 2018

    Leroux, J.: Polynomial vector addition systems with sta tes. In: Proceedings of ICALP 2018. vol. 107, pp. 134:1–134:13 (2018)

    work page 2018

  37. [37]

    In: Proceedings of LICS 2019 (2 019)

    Leroux, J., Schmitz, S.: Reachability in vector additio n systems is primitive- recursive in fixed dimension. In: Proceedings of LICS 2019 (2 019)

    work page 2019

  38. [38]

    Technical re- port 62 (1976)

    Lipton, R.: The reachability problem requires exponent ial space. Technical re- port 62 (1976)

    work page 1976

  39. [39]

    Mayr, E.: An algorithm for the general Petri net reachabi lity problem 13, 441–460 (1984)

    work page 1984

  40. [40]

    In: Proceedings of PLDI’1 8

    Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expect ations: Resource anal- ysis for probabilistic programs. In: Proceedings of PLDI’1 8. pp. 496–512. ACM, New York, NY, USA (2018)

    work page 2018

  41. [41]

    Puterman, M.: Markov Decision Processes (1994)

    work page 1994

  42. [42]

    Rackoff, C.: The covering and boundedness problems for ve ctor addition systems. Theor. Comput. Sci. 6, 223–231 (1978)

    work page 1978

  43. [43]

    ACM Trans

    Schmitz, S.: Complexity hierarchies beyond elementary . ACM Trans. Comput. The- ory 8(1), 3:1–3:36 (Feb 2016)

    work page 2016

  44. [44]

    In: Proccedin gs of CA V 2014

    Sinn, M., Zuleger, F., Veith, H.: A simple and scalable st atic analysis for bound analysis and amortized complexity analysis. In: Proccedin gs of CA V 2014. pp. 745–761 (2014)

    work page 2014

  45. [45]

    The MIT Press (2005)

    Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics (Intelligent Robotics and Autonomous Agents). The MIT Press (2005)

    work page 2005

  46. [46]

    Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.: The complexity of multi-mean-payoff and multi-energy ga mes. Inf. Comput. 241, 177–196 (2015)

    work page 2015

  47. [47]

    ACM Tran s

    Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thes ing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller , F., Puaut, I., Puschner, P., Staschulat, J., Stenstr¨ om, P.: The worst-ca se execution-time prob- lem—overview of methods and survey of tools. ACM Tran s. Embed. Com- put. Syst. 7(3), 36:1–36:53 (2008)

    work page 2008

  48. [48]

    Yen, H.C.: A unified approach for deciding the existence o f certain petri net paths. Inf. Comput. 96(1), 119–137 (1992) Deciding Fast Termination for Probabilistic V ASS 17 A Proofs We start by recalling basic notions of martingale theory. A stochast ic process m(0), m (1), m (2), . . . is a martingale if the following holds for all i ∈ N: – E[m(i)] < ∞ ,...

    work page 1992

  49. [49]

    For every strategy, the expected number of transitions from a transient state to some MEC state can be bounded by a constant k (a number dependent only on A and not the size of the initial configuration)

    work page

  50. [50]

    First, we consider the demonic case

    The asymptotic complexity of a MEC does not depend on the initial s tate. First, we consider the demonic case. In DAG-like V ASS-MDP, the only loops in the MEC decomposition are self-loops, i.e., once we leave MEC M and visit a different MEC M ′, we may never return to M . Moreover, there is a probability p < 1 such that for every MEC M and every strategy,...

    work page