Efficient analysis of probabilistic programs with an unbounded counter

DOI10.1145/2629599zbMATH Open1321.68186arXiv1102.2529OpenAlexW1975636681MaRDI QIDQ5501946FDOQ5501946

Authors: Tomáš Brázdil, Stefan Kiefer, Antonin Kučera 

Publication date: 14 August 2015

Published in: Journal of the ACM (Search for Journal in Brave)

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.

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

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

zbMATH Keywords

Markov chainsmodel checkingone-counter automata

Mathematics Subject Classification ID

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)

Cites Work

• Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Probability with Martingales
• Title not available (Why is that?)
• Title not available (Why is that?)
• A First Look at Rigorous Probability Theory
• On the Complexity of Numerical Analysis
• Generalized mean-payoff and energy games
• STACS 2005
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• One-counter stochastic games
• Energy parity games
• Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata

Cited In (7)

• 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
• Runtime analysis of probabilistic programs with unbounded recursion

Uses Software

• Rabinizer

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)