[HahnHWZ10] PASS: Abstraction Refinement for Infinite Probabilistic Models Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. 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.