Browse by author
Lookup NU author(s): Dr Sadegh SoudjaniORCiD
This is the authors' accepted manuscript of an article that has been published in its final definitive form by Society for Industrial and Applied Mathematics, 2013.
For re-use rights please refer to the publisher's terms and conditions.
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 contribution employs an abstraction procedure based on the partitioning of the state space, which generates a Markov chain as an approximation of the original process. The work puts forward a novel adaptive and sequential gridding algorithm that 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.
Author(s): Esmaeil Zadeh Soudjani S, Abate A
Publication type: Article
Publication status: Published
Journal: SIAM Journal on Applied Dynamical Systems
Year: 2013
Volume: 12
Issue: 2
Pages: 921-956
Online publication date: 22/03/2013
Date deposited: 08/11/2019
ISSN (electronic): 1536-0040
Publisher: Society for Industrial and Applied Mathematics
URL: https://doi.org/10.1137/120871456
DOI: 10.1137/120871456
Altmetrics provided by Altmetric
