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) are a popular model for concurrentsystems. However, many decision problems have prohibitively high complexity.Therefore, it is sometimes useful to consider overapproximating semantics inwhich these problems can be decided more efficiently.  We study an overapproximation, called monus semantics, that slightly relaxesthe semantics of decrements: A key property of a vector addition systems isthat in order to decrement a counter, this counter must have a positive value.In contrast, our semantics allows decrements of zero-valued counters: If such atransition is executed, the counter just remains zero.  It turns out that if only a subset of transitions is used with monussemantics (and the others with classical semantics), then reachability isundecidable. However, we show that if monus semantics is used throughout,reachability remains decidable. In particular, we show that reachability forVASS with monus semantics is as hard as that of classical VASS (i.e.Ackermann-hard), while the zero-reachability and coverability are easier (i.e.EXPSPACE-complete and NP-complete, respectively). We provide a comprehensiveaccount of the complexity of the general reachability problem, reachability ofzero configurations, and coverability under monus semantics. We study theseproblems in general VASS, two-dimensional VASS, and one-dimensional VASS, withunary and binary counter updates.

Monus semantics in vector addition systems with states