Deciding Fast Termination for Probabilistic VASS with Nondeterminism

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Antonín KUČERA, Petr NOVOTNÝ a 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, s. 462-478. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_27.

Základní údaje

Originální název

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Autoři

BRÁZDIL, Tomáš (203 Česká republika, domácí), Krishnendu CHATTERJEE (356 Indie), Antonín KUČERA (203 Česká republika, domácí), Petr NOVOTNÝ (203 Česká republika, garant, domácí) a Dominik VELAN (203 Česká republika, domácí)

Vydání

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

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107764

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-31783-6

ISSN

DOI

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

UT WoS

000723515700027

Klíčová slova anglicky

angelic and demonic nondeterminism; termination time; probabilistic VASS

Štítky

core_A, firank_A, formela-ver

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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

Česky

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.

---

Návaznosti

GA18-11193S, projekt VaV	Název: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy Investor: Grantová agentura ČR, Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy
GA19-15134Y, interní kód MU	Název: Verifikace a analýza pravděpodobnostních programů Investor: Grantová agentura ČR, Verifikace a analýza pravděpodobnostních programů
GJ19-15134Y, projekt VaV	Název: Verifikace a analýza pravděpodobnostních programů
MUNI/A/1018/2018, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII. Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1040/2018, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty