BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ and 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. p. nestránkováno, 10 pp. ISBN 978-1-4503-2886-9. doi:10.1145/2603088.2603161.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Zero-reachability in probabilistic multi-counter automata
Authors BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Stefan KIEFER (276 Germany), Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution), Petr NOVOTNÝ (203 Czech Republic, belonging to the institution) and Joost-Pieter KATOEN (528 Netherlands).
Edition 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), p. nestránkováno, 10 pp. 2014.
Publisher ACM
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
RIV identification code RIV/00216224:14330/14:00074099
Organization unit Faculty of Informatics
ISBN 978-1-4503-2886-9
Doi http://dx.doi.org/10.1145/2603088.2603161
Keywords in English markov chains; petri nets; reachability; multicounter automata
Tags best1, core_A, firank_1, formela-conference
Tags International impact, Reviewed
Changed by Changed by: RNDr. Petr Novotný, Ph.D., učo 172743. Changed: 16/11/2014 14:20.
Abstract
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.
Links
GPP202/12/P612, research and development projectName: Formální verifikace stochastických systémů s reálným časem (Acronym: Formální verifikace stochastických systémů s reáln)
Investor: Czech Science Foundation, Postdoctoral projects
MUNI/A/0765/2013, internal MU codeName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
MUNI/A/0855/2013, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 1/3/2021 09:23