Formal Abstraction and Synthesis of Parametric Stochastic Processes

Conference paper (2021)

Authors

A. Peruffo Team Manuel Mazo Jr - Mechanical, Maritime and Materials Engineering
Alessandro Abate University of Oxford
Research Group
Team Manuel Mazo Jr (Mechanical, Maritime and Materials Engineering) (TU Delft)
More Info
expand_more

Published Date

2021

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Mechanical, Maritime and Materials Engineering

Department

Delft Center for Systems and Control

Research Group

Team Manuel Mazo Jr

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.

Files

Peruffo_Abate2021_Chapter_Form... (.pdf)
(.pdf | 1.39 Mb)

Download not available