Zero-reachability in probabilistic multi-counter automata

DOI10.1145/2603088.2603161zbMATH Open1401.68151arXiv1401.6840OpenAlexW2122843152WikidataQ57800938 ScholiaQ57800938MaRDI QIDQ4635605FDOQ4635605

Stefan Kiefer, Tomáš Brázdil, Antonin Kučera, Petr Novotný, Joost-Pieter Katoen

Publication date: 23 April 2018

Published in: 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) (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1401.6840

zbMATH Keywords

Markov chainsreachabilitymulti-counter automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (6)

• Simple stochastic games with almost-sure energy-parity objectives are in NP and conp
• On the Existence and Computability of Long-Run Average Properties in Probabilistic VASS
• Introducing divergence for infinite probabilistic models
• Ratio and Weight Quantiles
• Probabilistic total store ordering
• Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models

This page was built for publication: Zero-reachability in probabilistic multi-counter automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635605)