Approximate abstractions of stochastic systems: a randomized method

This work introduces a randomized method for the design of an approximate abstraction of a stochastic system and the assessment of its quality. The proposed approach relies on the formulation of the problem as a semi-infinite chance-constrained optimization program and on its solution via randomization. The method has quite general applicability, since it only requires to be able to run multiple executions of the candidate abstract model and of the original system and to compute their distance. Two variants of the notion of distance are considered in view of a possible use of the approximate abstraction for probabilistic safety verification. The approach is tested on a numerical example.