License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.10
URN: urn:nbn:de:0030-drops-190047
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19004/
Baumann, Pascal ;
Madnani, Khushraj ;
Mazowiecki, Filip ;
Zetzsche, Georg
Monus Semantics in Vector Addition Systems with States
Abstract
Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently.
We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that 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 a transition is executed, the counter just remains zero.
It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS 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 comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.
BibTeX - Entry
@InProceedings{baumann_et_al:LIPIcs.CONCUR.2023.10,
author = {Baumann, Pascal and Madnani, Khushraj and Mazowiecki, Filip and Zetzsche, Georg},
title = {{Monus Semantics in Vector Addition Systems with States}},
booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-299-0},
ISSN = {1868-8969},
year = {2023},
volume = {279},
editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19004},
URN = {urn:nbn:de:0030-drops-190047},
doi = {10.4230/LIPIcs.CONCUR.2023.10},
annote = {Keywords: Vector addition systems, Overapproximation, Reachability, Coverability}
}
|
Keywords: |
|
Vector addition systems, Overapproximation, Reachability, Coverability |
|
Collection: |
|
34th International Conference on Concurrency Theory (CONCUR 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
07.09.2023 |
