Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2019

Kód důvěrnosti údajů

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

Název statě ve sborníku

Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings

ISBN

9783030317836

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

462-478

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Taipei, Taiwan

Datum konání akce

1. 1. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000723515700027