Formal Abstraction and Synthesis of Parametric Stochastic Processes

Abstract

Formal abstractions of stochastic difference equations (SDEs) translate continuous-space processes into finite-state Markov models that can be automatically model checked against probabilistic specifications. These formal procedures carry an abstraction error that can be used to refine the outcomes of the model checking procedure from the abstract model to the concrete SDE. Parameter synthesis techniques aim at finding (any or all) model parameters that ensure the validity of a given specification, and are currently investigated by and large for finite-state parametric Markov models. In this work instead, we consider classes of parametric SDEs, and develop specific abstraction procedures relating the parameters in the obtained finite-state models to those of the concrete SDEs; we further show how parameter synthesis on the abstract models can be used to assert the satisfaction of given formal properties on the original parametric SDEs.