with Lijun Zhang and Holger Hermanns,
Qest07 © IEEE Computer Society
Abstract. Probabilistic models are widely used to analyze embedded, networked, and more recently biological systems. Existing numerical analysis techniques are limited to finite-state models and suffer from the state explosion problem. As a consequence, the user often has to manually abstract the intended model to get a tractable one. To this end, we propose the predicate abstraction model checker PASS which automates this process. We leverage recent advances in automatic theorem proving to compute tractable finite-state models. Experiments show the feasibility of our approach. To the best of our knowledge, this is the first time that properties of probabilistic infinite-state models have been verified at this level of automation.
![[pdf.png]](images/pdf.png)
pdf
![[tex.png]](images/tex.png)
bib Links: [Google Scholar]