Sciweavers

QEST
2007
IEEE

Probabilistic Model Checking Modulo Theories

14 years 4 months ago
Probabilistic Model Checking Modulo Theories
— Probabilistic models are widely used to analyze embedded, networked, and more recently biological systems. Existing numerical analysis techniques are limited to finitestate models and suffer from the state explosion problem. As a nce, the user often has to manually abstract the intended model to get a tractable one. To this end, we propose the predicate ion 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.
Björn Wachter, Lijun Zhang, Holger Hermanns
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where QEST
Authors Björn Wachter, Lijun Zhang, Holger Hermanns
Comments (0)