




Publications  Zeroreachability in probabilistic multicounter automata





Reference:
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, Petr Novotný, and JoostPieter Katoen. Zeroreachability in probabilistic multicounter automata. In Proceedings of the Joint Meeting of the TwentyThird EACSL Annual Conference on Computer Science Logic (CSL) and the TwentyNinth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 22:1–22:10, Vienna, Austria, 2014.
Abstract:
We study the qualitative and quantitative zeroreachability problem in probabilistic multicounter 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 zeroreachability 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 zeroreaching 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 zeroreachability is decidable and SquareRootSumhard, and the probability of all zeroreaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 (these results apply 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.
Suggested BibTeX entry:
@inproceedings{14BKKNKLICS,
address = {Vienna, Austria},
author = {Tom\'a\v{s} Br\'azdil and Stefan Kiefer and Anton\'in Ku\v{c}era and Petr Novotn\'y and JoostPieter Katoen},
booktitle = {Proceedings of the Joint Meeting of the TwentyThird EACSL Annual Conference on Computer Science Logic (CSL) and the TwentyNinth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
pages = {22:122:10},
title = {Zeroreachability in probabilistic multicounter automata},
year = {2014}
}




