Zero-reachability in probabilistic multi-counter automata

DOI10.1145/2603088.2603161MaRDI QIDQ4635605zbMATH OpenOpenAlexWikidataFDO

Authors Tomáš Brázdil, Stefan Kiefer, Petr Novotný, Antonin Kučera, 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)

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)

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.

Recommendations

• One-counter Markov decision processes
• Counterexamples in Probabilistic Model Checking
• State explosion in almost-sure probabilistic reachability
• On Almost-Sure Properties of Probabilistic Discrete Event Systems
• The Reachability Problem for Vector Addition System with One Zero-Test

Cited in

(7)

• On the existence and computability of long-run average properties in probabilistic VASS
• Simple stochastic games with almost-sure energy-parity objectives are in NP and conp
• Ratio and weight quantiles
• Long-run average behaviour of probabilistic vector addition systems
• Introducing divergence for infinite probabilistic models
• 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)