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.
On-the-fly fast mean-field model-checking
Latella D;Massink M
2014
Abstract
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_279468-doc_78975.pdf
solo utenti autorizzati
Descrizione: On-the-fly fast mean-field model-checking
Tipologia:
Versione Editoriale (PDF)
Dimensione
463.16 kB
Formato
Adobe PDF
|
463.16 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.
