The Library
Reachability in fixed dimension vector addition systems with states
Tools
Czerwiński, Wojciech, Lasota, Slawomir, Lazic, Ranko, Leroux, Jerome and Mazowiecki, Filip (2020) Reachability in fixed dimension vector addition systems with states. In: 31st International Conference on Concurrency Theory (CONCUR 2020), Virtual conference, 01-04 Sep 2020. Published in: Leibniz International Proceedings in Informatics (LIPIcs), 171 doi:10.4230/LIPIcs.CONCUR.2020.48 ISSN 1868-8969.
|
PDF
WRAP-reachability-fixed-dimension-vector-addition-systems-states-Lazic-2020.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (704Kb) | Preview |
Official URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2020.48
Abstract
The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.
Item Type: | Conference Item (Paper) | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | |||||||||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | |||||||||||||||
Library of Congress Subject Headings (LCSH): | Machine theory, Computational complexity, Computable functions, Computer systems -- Verification, Petri nets | |||||||||||||||
Series Name: | Leibniz International Proceedings in Informatics | |||||||||||||||
Journal or Publication Title: | Leibniz International Proceedings in Informatics (LIPIcs) | |||||||||||||||
Publisher: | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik | |||||||||||||||
ISSN: | 1868-8969 | |||||||||||||||
Official Date: | 26 August 2020 | |||||||||||||||
Dates: |
|
|||||||||||||||
Volume: | 171 | |||||||||||||||
Article Number: | 48 | |||||||||||||||
DOI: | 10.4230/LIPIcs.CONCUR.2020.48 | |||||||||||||||
Status: | Peer Reviewed | |||||||||||||||
Publication Status: | Published | |||||||||||||||
Access rights to Published version: | Open Access (Creative Commons) | |||||||||||||||
Date of first compliant deposit: | 3 January 2019 | |||||||||||||||
Date of first compliant Open Access: | 16 January 2019 | |||||||||||||||
RIOXX Funder/Project Grant: |
|
|||||||||||||||
Conference Paper Type: | Paper | |||||||||||||||
Title of Event: | 31st International Conference on Concurrency Theory (CONCUR 2020) | |||||||||||||||
Type of Event: | Conference | |||||||||||||||
Location of Event: | Virtual conference | |||||||||||||||
Date(s) of Event: | 01-04 Sep 2020 | |||||||||||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year