1: \begin{abstract}

2:   This paper studies a difference operator for stochastic systems whose

3:   specifications are represented by Abstract Probabilistic Automata

4:   (APAs). In the case refinement fails between two specifications, the

5:   target of this operator is to produce a specification APA that

6:   represents all witness PAs of this failure.  Our contribution is an

7:   algorithm that permits to approximate the difference of two

8:   deterministic APAs with arbitrary precision. Our technique relies on

9:   new quantitative notions of distances between APAs used to assess

10:   convergence of the approximations, as well as on an in-depth

11:   inspection of the refinement relation for APAs. The procedure is

12:   effective and not more complex than refinement checking.

13: \end{abstract}

14: