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

作者：Soudjani Sadegh Esmaeil Zadeh^*; Abate Alessandro

来源：SIAM Journal on Applied Dynamical Systems, 2013, 12(2): 921-956.

DOI：10.1137/120871456

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

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.

• 出版日期2013