Efficient Analysis of Probabilistic Programs with an Unbounded Counter

DOI10.1145/2629599zbMath1321.68186arXiv1102.2529OpenAlexW1975636681MaRDI QIDQ5501946

Stefan Kiefer, Tomáš Brázdil, Antonín Kučera

Publication date: 14 August 2015

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

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

zbMATH Keywords

Markov chainsmodel checkingone-counter automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

On the Existence and Computability of Long-Run Average Properties in Probabilistic VASS, Probabilistic total store ordering, Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Uses Software

• Rabinizer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• One-Counter Stochastic Games
• Generalized Mean-payoff and Energy Games
• Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata
• A First Look at Rigorous Probability Theory
• Energy Parity Games
• On the Complexity of Numerical Analysis
• Probability with Martingales
• Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
• Tools and Algorithms for the Construction and Analysis of Systems
• STACS 2005