On-the-fly fast mean-field model-checking

Anovel,scalable,on-the-flymodel-checkingprocedureispre- sented 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 shown and some results of the applica- tion of a prototype implementation of the FlyFast model-checker are pre- sented.