On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination

• We show a new procedure combining on-the-fly model-checking and mean-field.
• We prove the asymptotic correctness of the on-the-fly model-checking procedure.
• We present a prototype implementation of the model-checking.
• We use the technique to analyze selection of simple and more elaborate scenarios.

Typical self-organising collective systems consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. Design of such systems is challenging and requires suitable, scalable analysis tools to check properties of proposed system designs before they are put into operation. We present a novel scalable, on-the-fly approximated model-checking procedure to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model-checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is proven and a prototype implementation of the model-checker is presented. The potential of the verification approach is illustrated by its application on self-organising collective systems and an overview of remaining open issues and future extensions is provided.