Mazowiecki, Filip, Sinclair-Banks, Henry and Wegrzycki, Karol (2023) Coverability in 2-VASS with one unary counter is in NP. In: 26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2023), Paris, France, 22-27 Apr 2023. Published in: Foundations of Software Science and Computation Structures. FoSSaCS 2023, 13992 pp. 196-217. ISBN 9783031308284. doi:10.1007/978-3-031-30829-1_10

Preview	PDF 978-3-031-30829-1_10.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (1277Kb) | Preview
	PDF WRAP-Coverability-2-VASS-one-unary-counter-NP-23.pdf - Accepted Version Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer. Download (810Kb)

Request Changes to record.

Abstract

Coverability in Petri nets finds applications in verification of safety properties of reactive systems. We study coverability in the equivalent model: Vector Addition Systems with States (VASS).

A k-VASS can be seen as k counters and a finite automaton whose transitions are labelled with k integers. Counter values are updated by adding the respective transition labels. A configuration in this system consists of a state and k counter values. Importantly, the counters are never allowed to take negative values. The coverability problem asks whether one can traverse the k-VASS from the initial configuration to a configuration with at least the counter values of the target.

In a well-established line of work on k-VASS, coverability in 2-VASS is already PSPACE-hard when the integer updates are encoded in binary. This lower bound limits the practicality of applications, so it is natural to focus on restrictions. In this paper we initiate the study of 2-VASS with one unary counter. Here, one counter receives binary encoded updates and the other receives unary encoded updates. Our main result is that coverability in 2-VASS with one unary counter is in NP. This improves upon the inherited state-of-the-art PSPACE upper bound. Our main technical contribution is that one only needs to consider runs in a certain compressed linear form.

Item Type:	Conference Item (Paper)
Subjects:	Q Science > QA Mathematics Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions:	Faculty of Science, Engineering and Medicine > Science > Computer Science Faculty of Science, Engineering and Medicine > Science > Mathematics
Library of Congress Subject Headings (LCSH):	Programming languages (Electronic computers), Computational complexity, Petri nets, Computer programming, Electronic data processing -- Distributed processing, Mathematical linguistics, Machine theory
Series Name:	Lecture Notes in Computer Science
Journal or Publication Title:	Foundations of Software Science and Computation Structures. FoSSaCS 2023
Publisher:	Springer
ISBN:	9783031308284
Official Date:	21 April 2023
Dates:	Date Event 21 April 2023 Published 22 December 2022 Accepted
Volume:	13992
Page Range:	pp. 196-217
DOI:	10.1007/978-3-031-30829-1_10
Status:	Peer Reviewed
Publication Status:	Published
Access rights to Published version:	Open Access (Creative Commons)
Date of first compliant deposit:	23 February 2023
Date of first compliant Open Access:	16 May 2023
RIOXX Funder/Project Grant:	Project/Grant ID RIOXX Funder Name Funder ID 950398 European Research Council http://dx.doi.org/10.13039/501100000781 EP/T5179X/1 [EPSRC] Engineering and Physical Sciences Research Council http://dx.doi.org/10.13039/501100000266 850979 European Research Council http://dx.doi.org/10.13039/501100000781
Conference Paper Type:	Paper
Title of Event:	26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2023)
Type of Event:	Conference
Location of Event:	Paris, France
Date(s) of Event:	22-27 Apr 2023

Request changes or add full text files to a record

Repository staff actions (login required)

View Item

Downloads