A novel, scalable, on-the-fly model-checking procedure is presented 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 application of a prototype implementation of the FlyFast model-checker are presented.
On-the-fly fast mean-field model-checking / Latella, Diego; Loreti, Michele; Massink, Mieke. - STAMPA. - (2014), pp. 297-314. [10.1007/978-3-319-05119-2_17]
On-the-fly fast mean-field model-checking
LORETI, MICHELE;
2014
Abstract
A novel, scalable, on-the-fly model-checking procedure is presented 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 application of a prototype implementation of the FlyFast model-checker are presented.
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
