PASS: Abstraction Refinement for Infinite Probabilistic Models

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

24 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings
Number of pages5
Publication statusPublished - 2010
Externally publishedYes


Dive into the research topics of 'PASS: Abstraction Refinement for Infinite Probabilistic Models'. Together they form a unique fingerprint.

Cite this