Structural Abstraction and Refinement for Probabilistic Programs
summary
Framework treats a Probabilistic Control‑Flow Automaton as an MDP whose actions drop semantics, so the structural upper bound is the MDP’s maximum reachability probability and over‑approximates violation. Refinement constructs automata (via interpolation and Floyd‑Hoare style trace abstraction) to remove infeasible nonviolating traces, yielding tighter bounds. Instantiation uses CEGAR with trace abstraction, leverages existing nonprobabilistic tools unchanged, and on benchmarks the tool solves ~2× more problems and is faster on 73% of cases.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:27Probabilistic threshold example
- 2:31PCFA and MDP relationship
- 5:47Upper bound for violation probability
- 8:23Structural refinement principles
- 9:26Refined automaton via trace abstraction
- 12:19Separating probability and semantics
- 13:46CIGAR automation and optimization
- 14:50Future directions and Q&A
related talks
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
21mMechanizing the CMP Abstraction for Parameterized Verification
20mNewtonian Program Analysis of Probabilistic Programs
18mQuantitative Bounds on Resource Usage of Probabilistic Programs
15mStatically Verified Refinements for Multiparty Protocols
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
19mSolving Infinite-State Games via Acceleration