English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Vector Addition Systems with States (VASS) consists of a finite state spaceequipped with d counters, where in each transition every counter isincremented, decremented, or left unchanged. VASS provide a fundamental modelfor analysis of concurrent processes, parametrized systems, and they are alsoused as abstract models for programs for bounds analysis. While termination isthe basic liveness property that asks the qualitative question of whether agiven model always terminates or not, the more general quantitative questionasks for bounds on the number of steps to termination. In the realm ofquantitative bounds a fundamental problem is to obtain asymptotic bounds ontermination time. Large asymptotic bounds such as exponential or higher alreadysuggest that either there is some error in modeling, or the model is not usefulin practice. Hence we focus on polynomial asymptotic bounds for VASS. Whilesome well-known approaches (e.g., lexicographic ranking functions) are neithersound nor complete with respect to polynomial bounds, other approaches onlypresent sound methods for upper bounds. In this work our main contributions areas follows: First, for linear asymptotic bounds we present a sound and completemethod for VASS, and moreover, our algorithm runs in polynomial time. Second,we classify VASS according the normals of the vectors of the cycles. We showthat singularities in the normal are the key reason for asymptotic bounds suchas exponential and non-elementary for VASS. In absence of singularities, weshow that the asymptotic complexity bound is always polynomial and of the form${\Theta}(n^k)$, for some k $\leq$ d. We present an algorithm, with timecomplexity polynomial in the size of the VASS and exponential in dimension d,to compute the optimal k.

Efficient Algorithms for Checking Fast Termination in VASS