Construction of Analyses.

We have used this approach to characterise various process equivalences in [29]. We have developed static analyses of probabilistic programs in [27] but these have been handcrafted. In the latter paper we have also used a form of widening operator to accelerate convergence. The linear algebraic setting that we work in gives us a way of measuring the distance between vectors and between operators; the appropriate notion of widening seems to be an operation that stabilises close to the answer rather than stabilising at an upper approximation (as in the order-theoretic framework). This will be investigated further and is a necessary prerequisite to us being able to use the probabilistic abstract interpretation framework to calculate analyses.