Stochastic Approximations in Model Checking: A New Scalable Approach to Collective Systems Verification

A collective system is a complex model comprised of a large number of individual entities, whose interaction gives rise to non-trivial emergent behaviours. The automatic verification of the intrinsically noisy dynamics of this type of models, by means of Stochastic Model Checking techniques, is severely hampered by the large size of their state space. In this project, we consider a new scalable and effective technique to validate the performance of these systems, based on Stochastic Approximations of the dynamics of the model. In this context, this works merges and extends the few preliminary results available in the literature at the beginning of this project and defines some interesting contributions leading the investigation in two major directions. First, we consider various types of Stochastic Approximations to accurately capture the probabilistic noise that characterises the evolution of collective systems when the number of individuals in the population is limited (mesoscopic collective systems). Second, we extend the set of properties that can be validated exploiting the efficiency of Stochastic Approximations. In particular, we consider requirements on the behaviour of the individuals (local properties), of the population (global properties) and of the individuals in the global context (local-to-global properties). Moreover, we develop procedures to verify the dynamics of time-critical systems. Finally, we prove the theoretical results that guarantee the quality of the developed model checking procedures, showing the asymptotic convergence of the results and the exactness in the limit of an infinite population size.