[HahnHWZ10]
PASS: Abstraction Refinement for Infinite Probabilistic
Models
In Tools and Algorithms for the Construction and Analysis of
Systems, 16th International Conference (TACAS), pages 353-357, Springer, Lecture Notes in Computer Science 6015, 2010.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-12002-2_30
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. PASS has been successfully
applied to network protocols and serves as a test platform for different
refinement methods.