Structural Abstraction and Refinement for Probabilistic Programs

TL;DR

This paper introduces a structural abstraction refinement framework for verifying probabilistic programs, using MDPs to efficiently compute upper bounds on violation probabilities and enabling the use of non-probabilistic techniques.

Contribution

It presents a novel structural approach that separates probabilistic and semantic concerns, allowing flexible verification of probabilistic programs via CEGAR and trace abstraction.

Findings

Effective in handling diverse probabilistic programs

Outperforms state-of-the-art tools in speed and flexibility

Enables reuse of non-probabilistic verification techniques

Abstract

In this paper, we present structural abstraction refinement, a novel framework for verifying the threshold problem of probabilistic programs. Our approach represents the structure of a Probabilistic Control-Flow Automaton (PCFA) as a Markov Decision Process (MDP) by abstracting away statement semantics. The maximum reachability of the MDP naturally provides a proper upper bound of the violation probability, termed the structural upper bound. This introduces a fresh ``structural'' characterization of the relationship between PCFA and MDP, contrasting with the traditional ``semantical'' view, where the MDP reflects semantics. The method uniquely features a clean separation of concerns between probability and computational semantics that the abstraction focuses solely on probabilistic computation and the refinement handles only the semantics aspect, where the latter allows non-random program verification techniques to be employed without modification. Building upon this feature, we propose a general counterexample-guided abstraction refinement (CEGAR) framework, capable of leveraging established non-probabilistic techniques for probabilistic verification. We explore its instantiations using trace abstraction. Our method was evaluated on a diverse set of examples against state-of-the-art tools, and the experimental results highlight its versatility and ability to handle more flexible structures swiftly.