Deciding Fast Termination for Probabilistic VASS with
Nondeterminism

D 2019

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Antonín KUČERA, Petr NOVOTNÝ, Dominik VELAN et. al.

Basic information

Original name

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Authors

BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Krishnendu CHATTERJEE (356 India), Antonín KUČERA (203 Czech Republic, belonging to the institution), Petr NOVOTNÝ (203 Czech Republic, guarantor, belonging to the institution) and Dominik VELAN (203 Czech Republic, belonging to the institution)

Edition

Cham, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings, p. 462-478, 17 pp. 2019

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00107764

Organization unit

Faculty of Informatics

ISBN

978-3-030-31783-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-31784-3_27

UT WoS

000723515700027

Keywords in English

angelic and demonic nondeterminism; termination time; probabilistic VASS

Abstract

ORIG CZ

V originále

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).

In Czech

V článku je studována problematika asymptotického odhadu očekávané doby terminace daného VASS systému obohaceného o stochastické stavy.

Links

GA18-11193S, research and development project

Name: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Investor: Czech Science Foundation

GA19-15134Y, interní kód MU

Name: Verifikace a analýza pravděpodobnostních programů

Investor: Czech Science Foundation

GJ19-15134Y, research and development project

Name: Verifikace a analýza pravděpodobnostních programů

MUNI/A/1018/2018, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masaryk University, Category A

MUNI/A/1040/2018, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Antonín KUČERA, Petr NOVOTNÝ and Dominik VELAN. Deciding Fast Termination for Probabilistic VASS with Nondeterminism. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings. Cham: Springer, 2019, p. 462-478. ISBN 978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3_27.

@inproceedings{1576916,
   author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Kučera, Antonín and Novotný, Petr and Velan, Dominik},
   address = {Cham},
   booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-31784-3_27},
   editor = {Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza},
   keywords = {angelic and demonic nondeterminism; termination time; probabilistic VASS},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-31783-6},
   pages = {462-478},
   publisher = {Springer},
   title = {Deciding Fast Termination for Probabilistic VASS with Nondeterminism},
   url = {https://doi.org/10.1007/978-3-030-31784-3_27},
   year = {2019}
}

TY  - JOUR
ID  - 1576916
AU  - Brázdil, Tomáš - Chatterjee, Krishnendu - Kučera, Antonín - Novotný, Petr - Velan, Dominik
PY  - 2019
TI  - Deciding Fast Termination for Probabilistic VASS with Nondeterminism
PB  - Springer
CY  - Cham
SN  - 9783030317836
KW  - angelic and demonic nondeterminism
KW  - termination time
KW  - probabilistic VASS
UR  - https://doi.org/10.1007/978-3-030-31784-3_27
L2  - https://doi.org/10.1007/978-3-030-31784-3_27
N2  - 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).
ER  -

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Antonín KUČERA, Petr NOVOTNÝ and Dominik VELAN. Deciding Fast Termination for Probabilistic VASS with Nondeterminism. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. \textit{Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings}. Cham: Springer, 2019, p.~462-478. ISBN~978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3\_{}27.

Detailed Information on Publication Record