TY - GEN
T1 - Formal Abstraction and Synthesis of Parametric Stochastic Processes
AU - Peruffo, Andrea
AU - Abate, Alessandro
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85115189551&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-85037-1_9
DO - 10.1007/978-3-030-85037-1_9
M3 - Conference contribution
AN - SCOPUS:85115189551
SN - 978-3-030-85036-4
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 135
EP - 153
BT - Formal Modeling and Analysis of Timed Systems - 19th International Conference, FORMATS 2021, Proceedings
A2 - Dima, Catalin
A2 - Shirmohammadi, Mahsa
PB - Springer
T2 - 19th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2021
Y2 - 24 August 2021 through 26 August 2021
ER -