Bounded model checking for probabilistic programs

DOI10.1007/978-3-319-46520-3_5MaRDI QIDQ1990501zbMATH OpenOpenAlexFDO

Authors Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Lukas Westhofen, Joost-Pieter Katoen

Publication date 25 October 2018

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard probabilistic program is a potentially infinite parametric Markov decision process, no direct adaption of existing techniques is possible. Therefore, we propose an on-the-fly approach where the operational model is successively created and verified via a step-wise execution of the program. This approach enables to take key features of many probabilistic programs into account: nondeterminism and conditioning. We discuss the restrictions and demonstrate the scalability on several benchmarks.

Recommendations

• Validation of Stochastic Systems
• Verification of Probabilistic Programs
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Model checking probabilistic systems
• The probabilistic model checking landscape

Cited in

(21)

• Probabilistic black-box reachability checking (extended version)
• Time-bounded termination analysis for probabilistic programs with delays
• Preface to the special issue on probabilistic model checking
• A progress measure for explicit-state probabilistic model-checkers
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Symbolic bounded conformance checking of model programs
• A bounded model checker for SPARK programs
• Probabilistic programming: a true verification challenge
• Model checking with probabilistic tabled logic programming
• Probabilistic abstraction for model checking: an approach based on property testing
• Validation of Stochastic Systems
• Counterexamples in Probabilistic Model Checking
• A debugger for probabilistic programs
• Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic
• Probabilistic Metric Temporal Graph Logic
• Does a Program Yield the Right Distribution?
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Constraint-based debugging in probabilistic model checking
• Generating counterexamples for quantitative safety specifications in probabilistic B
• Under-approximating expected total rewards in POMDPs
• Latticed \(k\)-induction with an application to probabilistic programs

This page was built for publication: Bounded model checking for probabilistic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1990501)