PASS: Abstraction Refinement for Infinite Probabilistic Models

Ernst Moritz  Hahn; Holger Hermanns; Bjorn Wachter; Lijun Zhang

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

PASS: Abstraction Refinement for Infinite Probabilistic Models

Ernst Moritz Hahn, Holger Hermanns, Bjorn Wachter, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

26 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
Subtitle of host publication	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
Publisher	Springer
Pages	353-357
ISBN (Electronic)	978-3-642-12002-2
ISBN (Print)	978-3-642-12001-5
DOIs	https://doi.org/10.1007/978-3-642-12002-2_30
Publication status	Published - 2010
Externally published	Yes
Event	16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 - Paphos, Cyprus Duration: 20 Mar 2010 → 28 Mar 2010 Conference number: 16 http://www.etaps.org/2010/Conf/conf-frame-tacas.html

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	6015
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010
Abbreviated title	TACAS
Country/Territory	Cyprus
City	Paphos
Period	20/03/10 → 28/03/10
Internet address	http://www.etaps.org/2010/Conf/conf-frame-tacas.html

Access to Document

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

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). (Lecture Notes in Computer Science; Vol. 6015). Springer. https://doi.org/10.1007/978-3-642-12002-2_30

Hahn, Ernst Moritz ; Hermanns, Holger ; Wachter, Bjorn et al. / 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. Springer, 2010. pp. 353-357 (Lecture Notes in Computer Science).

@inproceedings{12510ccb685f42e7b74692c0858192e1,

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 Bjorn Wachter and Lijun Zhang",

year = "2010",

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

language = "English",

isbn = "978-3-642-12001-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "353--357",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

note = "16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, TACAS ; Conference date: 20-03-2010 Through 28-03-2010",

url = "http://www.etaps.org/2010/Conf/conf-frame-tacas.html",

}

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. Lecture Notes in Computer Science, vol. 6015, Springer, pp. 353-357, 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Paphos, Cyprus, 20/03/10. https://doi.org/10.1007/978-3-642-12002-2_30

PASS: Abstraction Refinement for Infinite Probabilistic Models. / Hahn, Ernst Moritz ; Hermanns, Holger; Wachter, Bjorn et al.
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. Springer, 2010. p. 353-357 (Lecture Notes in Computer Science; Vol. 6015).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - PASS: Abstraction Refinement for Infinite Probabilistic Models

AU - Hahn, Ernst Moritz

AU - Hermanns, Holger

AU - Wachter, Bjorn

AU - Zhang, Lijun

N1 - Conference code: 16

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

SN - 978-3-642-12001-5

T3 - Lecture Notes in Computer Science

SP - 353

EP - 357

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer

T2 - 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010

Y2 - 20 March 2010 through 28 March 2010

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. Springer. 2010. p. 353-357. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-12002-2_30