Model Checking Markov Population Models by Stochastic Approximations
Abstract
Many complex systems can be described by population models, in which a pool of agents interacts and produces complex collective behaviours. We consider the problem of verifying formal properties of the underlying mathematical representation of these models, which is a Continuous Time Markov Chain, often with a huge state space. To circumvent the state space explosion, we rely on stochastic approximation techniques, which replace the large model by a simpler one, guaranteed to be probabilistically consistent. We show how to efficiently and accurately verify properties of random individual agents, specified by Continuous Stochastic Logic extended with Timed Automata (CSL-TA), and how to lift these specifications to the collective level, approximating the number of agents satisfying them using second or higher order stochastic approximation techniques.
Cite
@article{arxiv.1711.03826,
title = {Model Checking Markov Population Models by Stochastic Approximations},
author = {Luca Bortolussi and Roberta Lanciani and Laura Nenzi},
journal= {arXiv preprint arXiv:1711.03826},
year = {2017}
}