Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the longrun average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) longrun emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lassoshaped) computation such that the longrun average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular longrun emptiness problem is (a) decidable in polynomial time for integervalued VASS, and (b) decidable but nonelementarily hard for naturalvalued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NPcomplete for integervalued VASS, and (d) undecidable for naturalvalued VASS. Our most interesting result is for (c) integervalued VASS with general cost functions, where we establish a connection between the regular longrun emptiness problem and quadratic Diophantine inequalities. The general (nonregular) longrun emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.
BibTeX  Entry
@InProceedings{chatterjee_et_al:LIPIcs:2019:10929,
author = {Krishnendu Chatterjee and Thomas A. Henzinger and Jan Otop},
title = {{LongRun Average Behavior of Vector Addition Systems with States}},
booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)},
pages = {27:127:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771214},
ISSN = {18688969},
year = {2019},
volume = {140},
editor = {Wan Fokkink and Rob van Glabbeek},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10929},
URN = {urn:nbn:de:0030drops109293},
doi = {10.4230/LIPIcs.CONCUR.2019.27},
annote = {Keywords: vector addition systems, meanpayoff, Diophantine inequalities}
}
Keywords: 

vector addition systems, meanpayoff, Diophantine inequalities 
Collection: 

30th International Conference on Concurrency Theory (CONCUR 2019) 
Issue Date: 

2019 
Date of publication: 

20.08.2019 