Efficient Algorithms for Checking Fast Termination in VASS
Tom\'a\v{s} Br\'azdil, Krishnendu Chatterjee, Anton\'in Ku\v{c}era,, Petr Novotn\'y, Dominik Velan

TL;DR
This paper introduces a polynomial-time, sound, and complete method for determining linear asymptotic bounds on termination time in VASS, classifies VASS based on cycle vector normals, and identifies singularities as key to complex bounds.
Contribution
It provides the first polynomial-time algorithm for linear asymptotic bounds in VASS and classifies VASS complexity based on cycle normal singularities.
Findings
Polynomial-time algorithm for linear bounds in VASS
Singularities in cycle normals lead to exponential bounds
Absence of singularities guarantees polynomial bounds of form Θ(n^k)
Abstract
Vector Addition Systems with States (VASS) consists of a finite state space equipped with d counters, where in each transition every counter is incremented, decremented, or left unchanged. VASS provide a fundamental model for analysis of concurrent processes, parametrized systems, and they are also used as abstract models for programs for bounds analysis. While termination is the basic liveness property that asks the qualitative question of whether a given model always terminates or not, the more general quantitative question asks for bounds on the number of steps to termination. In the realm of quantitative bounds a fundamental problem is to obtain asymptotic bounds on termination time. Large asymptotic bounds such as exponential or higher already suggest that either there is some error in modeling, or the model is not useful in practice. Hence we focus on polynomial asymptotic bounds…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Real-Time Systems Scheduling · Logic, programming, and type systems
