Efficient analysis of probabilistic programs with an unbounded counter
From MaRDI portal
Publication:5501946
Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
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
- 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?)
- A First Look at Rigorous Probability Theory
- Energy parity games
- Generalized mean-payoff and energy games
- 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
(7)- Runtime analysis of probabilistic programs with unbounded recursion
- On the existence and computability of long-run average properties in probabilistic VASS
- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- Runtime analysis of probabilistic programs with unbounded recursion
- Introducing divergence for infinite probabilistic models
- Probabilistic total store ordering
- Deciding fast termination for probabilistic VASS with nondeterminism
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)
