Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes

Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes

Esmaeil Zadeh Soudjani, S.
Abate, A.

Mechanical, Maritime and Materials Engineering

Delft Center for Systems and Control

2013-06-19

This work is concerned with the generation of finite abstractions of general state-space processes to be employed in the formal verification of probabilistic properties by means of automatic techniques such as probabilistic model checkers. The work employs an abstraction procedure based on the partitioning of the state-space, which generates a Markov chain as an approximation of the original process. A novel adaptive and sequential gridding algorithm is presented and is expected to conform to the underlying dynamics of the model and thus to mitigate the curse of dimensionality unavoidably related to the partitioning procedure. The results are also extended to the general modeling framework known as stochastic hybrid systems. While the technique is applicable to a wide arena of probabilistic properties, with focus on the study of a particular specification (probabilistic safety, or invariance, over a finite horizon), the proposed adaptive algorithm is first benchmarked against a uniform gridding approach taken from the literature and finally tested on an applicative case study in Biology.

general state-space processes
Markov chains
stochastic hybrid systems
abstractions
approximations
formal verification
safety and invariance
properties and specifications

http://resolver.tudelft.nl/uuid:bfc36534-6546-4173-be20-c08d0aff2ee7

https://doi.org/10.1137/120871456

Society for Industrial and Applied Mathematics (SIAM)

1536-0040

https://doi.org/10.1137/120871456

SIAM Journal on Applied Dynamical Systems, 12 (2), 2013

Institutional Repository

journal article

© 2013 SIAM