Presentation: Roberta Lanciani

Stochastic Approximations and Verifications

In this talk, we discuss the use of stochastic approximations to validate properties of Markov population models. This type of Markovian models are used to describe the evolution of large systems of interacting entities, and their verification, using standard stochastic model checking techniques, is ampered by the large number of possible behavious of the agents in the population, which leads to the well known curse of the state space explosion. To tackle this problem, we define new model checking procedures based on different types of stochastic approximations, namely the Fluid, the Central Limit and the Higher Orders Approximations, which can be used to accurately and efficiently extimate the evolution of large population models. In this talk, we introduce these model checking techniques, reviewing the type of properties that can be verified, the definition of the stochastic approximations, and some results obtained on a simple epidemic model.

Bookmark the permalink.