Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00107764" target="_blank" >RIV/00216224:14330/19:00107764 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-030-31784-3_27" target="_blank" >https://doi.org/10.1007/978-3-030-31784-3_27</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-31784-3_27" target="_blank" >10.1007/978-3-030-31784-3_27</a>

Result language
angličtina
Original language name
Deciding Fast Termination for Probabilistic VASS with Nondeterminism
Original language description
A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Omega(n^2).
Czech name
—
Czech description
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings
ISBN
9783030317836
ISSN
0302-9743
e-ISSN
—
Number of pages
17
Pages from-to
462-478
Publisher name
Springer
Place of publication
Cham
Event location
Taipei, Taiwan
Event date
Jan 1, 2019
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000723515700027

Similar results(10)