BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ a Joost-Pieter KATOEN. Zero-reachability in probabilistic multi-counter automata. In Thomas Henzinger and Dale Miller. 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). New York: ACM, 2014. s. nestránkováno, 10 s. ISBN 978-1-4503-2886-9. doi:10.1145/2603088.2603161.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Zero-reachability in probabilistic multi-counter automata
Autoři BRÁZDIL, Tomáš (203 Česká republika, domácí), Stefan KIEFER (276 Německo), Antonín KUČERA (203 Česká republika, garant, domácí), Petr NOVOTNÝ (203 Česká republika, domácí) a Joost-Pieter KATOEN (528 Nizozemsko).
Vydání New York, 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), od s. nestránkováno, 10 s. 2014.
Nakladatel ACM
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání elektronická verze "online"
WWW URL
Kód RIV RIV/00216224:14330/14:00074099
Organizační jednotka Fakulta informatiky
ISBN 978-1-4503-2886-9
Doi http://dx.doi.org/10.1145/2603088.2603161
Klíčová slova anglicky markov chains; petri nets; reachability; multicounter automata
Štítky best1, core_A, firank_1, formela-conference
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Petr Novotný, Ph.D., učo 172743. Změněno: 16. 11. 2014 14:20.
Anotace
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. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.
Návaznosti
GPP202/12/P612, projekt VaVNázev: Formální verifikace stochastických systémů s reálným časem (Akronym: Formální verifikace stochastických systémů s reáln)
Investor: Grantová agentura ČR, Postdoktorské projekty
MUNI/A/0765/2013, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0855/2013, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 2. 3. 2021 19:22