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 - Extended version
Latella D;Massink M
2013
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_276691-doc_78617.pdf
solo utenti autorizzati
Descrizione: On-the-fly fast mean-field model-checking - Extended version
Dimensione
701.3 kB
Formato
Adobe PDF
|
701.3 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
