PASS: Abstraction Refinement for Infinite Probabilistic Models

Abstract

We present PASS, a tool that analyzes concurrent probabilistic programs, which map to potentially infinite Markov decision processes. PASS is based on predicate abstraction and abstraction refinement and scales to programs far beyond the reach of numerical methods which operate on the full state space of the model. The computational engines we use are SMT solvers to compute finite abstractions, numerical methods to compute probabilities and interpolation as part of abstraction refinement. sf PASS has been successfully applied to network protocols and serves as a test platform for different refinement methods