Model Checking Markov Population Models by Stochastic Approximations

TL;DR

This paper presents a method for verifying properties of large population models by using stochastic approximation techniques to efficiently analyze complex Markov models with large state spaces.

Contribution

It introduces a stochastic approximation approach for verifying properties of population models represented by large CTMCs, enabling scalable analysis.

Findings

Efficient verification of individual agent properties using CSL-TA.

Approximation of collective agent behaviors with second or higher order stochastic methods.

Guarantees probabilistic consistency despite model simplification.

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.