PASS: Abstraction Refinement for Infinite Probabilistic Models

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication16th 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
PublisherSpringer
Pages353-357
ISBN (Electronic)978-3-642-12002-2
ISBN (Print)978-3-642-12001-5
DOIs
Publication statusPublished - 2010
Externally publishedYes
Event16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 - Paphos, Cyprus
Duration: 20 Mar 201028 Mar 2010
Conference number: 16
http://www.etaps.org/2010/Conf/conf-frame-tacas.html

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6015
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010
Abbreviated titleTACAS
CountryCyprus
CityPaphos
Period20/03/1028/03/10
Internet address

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

Cite this