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.
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination
Latella D;Massink M
2015
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
prod_333558-doc_103560.pdf
solo utenti autorizzati
Descrizione: On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination
Tipologia:
Versione Editoriale (PDF)
Dimensione
911.94 kB
Formato
Adobe PDF
|
911.94 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
prod_333558-doc_159220.pdf
accesso aperto
Descrizione: preprint version
Tipologia:
Versione Editoriale (PDF)
Dimensione
703.28 kB
Formato
Adobe PDF
|
703.28 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.