Efficient analysis of probabilistic programs with an unbounded counter
From MaRDI portal
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Abstract: We show that a subclass of infinite-state probabilistic programs that can be modeled by probabilistic one-counter automata (pOC) admits an efficient quantitative analysis. In particular, we show that the expected termination time can be approximated up to an arbitrarily small relative error with polynomially many arithmetic operations, and the same holds for the probability of all runs that satisfy a given omega-regular property. Further, our results establish a powerful link between pOC and martingale theory, which leads to fundamental observations about quantitative properties of runs in pOC. In particular, we provide a "divergence gap theorem", which bounds a positive non-termination probability in pOC away from zero.
Recommendations
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- Runtime analysis of probabilistic programs with unbounded recursion
- Runtime analysis of probabilistic programs with unbounded recursion
- Reasoning about Recursive Probabilistic Programs
- Weakest precondition reasoning for expected run-times of probabilistic programs
Cites work
- A First Look at Rigorous Probability Theory
- Energy parity games
- Generalized mean-payoff and energy games
- scientific article; zbMATH DE number 1670780 (Why is no real title available?)
- scientific article; zbMATH DE number 3145626 (Why is no real title available?)
- scientific article; zbMATH DE number 5485454 (Why is no real title available?)
- scientific article; zbMATH DE number 3664335 (Why is no real title available?)
- scientific article; zbMATH DE number 3736680 (Why is no real title available?)
- scientific article; zbMATH DE number 3269388 (Why is no real title available?)
- On the Complexity of Numerical Analysis
- One-counter stochastic games
- Probability with Martingales
- Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
- STACS 2005
- Tools and Algorithms for the Construction and Analysis of Systems
- Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata
Cited in
(8)- On the existence and computability of long-run average properties in probabilistic VASS
- Runtime analysis of probabilistic programs with unbounded recursion
- Deciding fast termination for probabilistic VASS with nondeterminism
- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- Probabilistic total store ordering
- Introducing divergence for infinite probabilistic models
- About decisiveness of dynamic probabilistic models
- Runtime analysis of probabilistic programs with unbounded recursion
This page was built for publication: Efficient analysis of probabilistic programs with an unbounded counter
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5501946)
