Zero-reachability in probabilistic multi-counter automata
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00074099" target="_blank" >RIV/00216224:14330/14:00074099 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1145/2603088.2603161" target="_blank" >http://dx.doi.org/10.1145/2603088.2603161</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/2603088.2603161" target="_blank" >10.1145/2603088.2603161</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Zero-reachability in probabilistic multi-counter automata
Popis výsledku v původním jazyce
We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 in time which is polynomial in log(epsilon), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter.
Název v anglickém jazyce
Zero-reachability in probabilistic multi-counter automata
Popis výsledku anglicky
We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 in time which is polynomial in log(epsilon), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GPP202%2F12%2FP612" target="_blank" >GPP202/12/P612: Formální verifikace stochastických systémů s reálným časem</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2014
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
ISBN
9781450328869
ISSN
—
e-ISSN
—
Počet stran výsledku
10
Strana od-do
—
Název nakladatele
ACM
Místo vydání
New York
Místo konání akce
Vídeň
Datum konání akce
1. 1. 2014
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—