Probabilistic Abstractions with Arbitrary Domains

TL;DR

This paper introduces a new probabilistic abstraction technique that leverages arbitrary abstract domains and widening operators, enabling more effective loop invariant discovery and refinement in probabilistic program analysis.

Contribution

It extends probabilistic abstraction methods beyond predicate abstraction by utilizing abstract reachability trees and suitable widening operators.

Findings

Enables use of arbitrary abstract domains in probabilistic analysis.

Improves loop invariant detection through novel widening techniques.

Provides refinement strategies for probabilistic program verification.

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 diffcult to find for predicate abstraction, and propose refinement techniques.