Reference:

Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011.

Abstract:

Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to predicate abstraction. We present a novel technique, based on the abstract reachability tree recently introduced by Gulavani et al., that can use arbitrary abstract domains and widening operators (in the sense of Abstract Interpretation). We show how suitable widening operators can deduce loop invariants difficult to find for predicate abstraction, and propose refinement techniques.

Suggested BibTeX entry:

@inproceedings{EG10Sas,
    address = {Venice, Italy},
    author = {Javier Esparza and Andreas Gaiser},
    booktitle = {Proceedings of the 18th International Static Analysis Symposium (SAS)},
    month = {September},
    title = {Probabilistic Abstractions with Arbitrary Domains},
    year = {2011}
}