Reference:

Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010.

Abstract:

Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. In these approaches, programs are abstracted into Markov Decision Processes (MDPs). Analysis of the MDPs allows to compute lower and upper bounds for the probability of reaching an error state. The bounds can be improved by refining the abstraction. The approaches of Hermanns et al. and Kattenbelt et al. 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 several refinement techniques.

Suggested BibTeX entry:

@techreport{EG10:TechRep,
    author = {Javier Esparza and Andreas Gaiser},
    institution = {Technische Universit{\"a}t M{\"u}nchen, Institut f\"{u}r Informatik},
    month = {December},
    title = {Probabilistic Abstractions with Arbitrary Domains},
    year = {2010}
}