Reference
[WachterZH07] Probabilistic Model Checking Modulo Theories. In Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems, 2007.Downloads: pdf, bibAbstract. 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.
