Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multidimensional longrun average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the longrun average value of a computation for the counter is the longrun average of the costs of the configurations in the computation. The multidimensional longrun average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the longrun average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected longrun average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multidimensional longrun average problem (a) is NPcomplete for integervalued VASS; (b) is undecidable for naturalvalued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integervalued VASS, and probabilistic naturalvalued VASS when all computations are nonterminating.
BibTeX  Entry
@InProceedings{chatterjee_et_al:LIPIcs:2020:12835,
author = {Krishnendu Chatterjee and Thomas A. Henzinger and Jan Otop},
title = {{MultiDimensional LongRun Average Problems for Vector Addition Systems with States}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {23:123:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771603},
ISSN = {18688969},
year = {2020},
volume = {171},
editor = {Igor Konnov and Laura Kov{\'a}cs},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12835},
URN = {urn:nbn:de:0030drops128359},
doi = {10.4230/LIPIcs.CONCUR.2020.23},
annote = {Keywords: vector addition systems, meanpayoff, multidimension, probabilistic semantics}
}
Keywords: 

vector addition systems, meanpayoff, multidimension, probabilistic semantics 
Collection: 

31st International Conference on Concurrency Theory (CONCUR 2020) 
Issue Date: 

2020 
Date of publication: 

26.08.2020 