PASS: Abstraction Refinement for Infinite Probabilistic Models

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

doi:10.1007/978-3-642-12002-2_30

PASS: Abstraction Refinement for Infinite Probabilistic Models

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

24 Citations (Scopus)

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.

Original language	English
Title of host publication	Tools 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
Pages	353-357
Number of pages	5
DOIs	https://doi.org/10.1007/978-3-642-12002-2_30
Publication status	Published - 2010
Externally published	Yes

Access to Document

10.1007/978-3-642-12002-2_30

https://doi.org/10.1007/978-3-642-12002-2_30

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

Cite this

Hahn, E. M., Hermanns, H., Wachter, B., & Zhang, L. (2010). PASS: Abstraction Refinement for Infinite Probabilistic Models. In Tools 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 (pp. 353-357) https://doi.org/10.1007/978-3-642-12002-2_30

Hahn, Ernst Moritz ; Hermanns, Holger ; Wachter, Björn ; Zhang, Lijun. / PASS: Abstraction Refinement for Infinite Probabilistic Models. Tools 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. 2010. pp. 353-357

@inproceedings{3a83791206d64102877a02fb6a045b31,

title = "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.",

author = "Hahn, {Ernst Moritz} and Holger Hermanns and Bj{\"o}rn Wachter and Lijun Zhang",

year = "2010",

doi = "10.1007/978-3-642-12002-2_30",

language = "English",

pages = "353--357",

booktitle = "Tools 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",

}

Hahn, EM, Hermanns, H, Wachter, B & Zhang, L 2010, PASS: Abstraction Refinement for Infinite Probabilistic Models. in Tools 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. pp. 353-357. https://doi.org/10.1007/978-3-642-12002-2_30

PASS: Abstraction Refinement for Infinite Probabilistic Models. / Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn; Zhang, Lijun.

Tools 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. 2010. p. 353-357.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - PASS: Abstraction Refinement for Infinite Probabilistic Models

AU - Hahn, Ernst Moritz

AU - Hermanns, Holger

AU - Wachter, Björn

AU - Zhang, Lijun

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-12002-2_30

DO - 10.1007/978-3-642-12002-2_30

M3 - Conference contribution

SP - 353

EP - 357

BT - Tools 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

ER -

Hahn EM, Hermanns H, Wachter B, Zhang L. PASS: Abstraction Refinement for Infinite Probabilistic Models. In Tools 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. 2010. p. 353-357 https://doi.org/10.1007/978-3-642-12002-2_30