On-the-fly PCTL fast mean-field model-checking for self-organising coordination - Preliminary version (Rapporti tecnici/preprint/working paper)

Type

• Rapporti tecnici/preprint/working paper (Classe)
• Prodotto della ricerca (Classe)

Label

• On-the-fly PCTL fast mean-field model-checking for self-organising coordination - Preliminary version (Rapporti tecnici/preprint/working paper) (literal)

Anno

• 2013-01-01T00:00:00+01:00 (literal)

Alternative label

• Latella D., Loreti M., Massink M. (2013)
  On-the-fly PCTL fast mean-field model-checking for self-organising coordination - Preliminary version
  
  (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

• Latella D., Loreti M., Massink M. (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#altreInformazioni

• Progetto A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours Acronimo QUANTICOL Grant agreement 600708 (literal)

Note

• PuMa (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#supporto

• Altro (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni

• CNR-ISTI, Pisa, Italy; Università di Firenze, Italy; CNR-ISTI, Pisa, Italy. (literal)

Titolo

• On-the-fly PCTL fast mean-field model-checking for self-organising coordination - Preliminary version (literal)

Abstract

• Typical self-organising collective systems consist of a large number of inter- acting 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. The exploitation of mean field approximation in model-checking techniques seems a promising approach to overcome scal- ability issues raised by the size of such collective systems. We present a novel scalable, on-the-fly model-checking procedure to verify bounded PCTL properties of selected individuals in the context of very large systems of in- dependent 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 several self- organising collective systems and an overview of remaining open issues and future extensions is provided. (literal)

Prodotto di

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)

Insieme di parole chiave

• Parole chiave di "On-the-fly PCTL fast mean-field model-checking for self-organising coordination - Preliminary version" (Insieme di parole chiave)

Incoming links:

Autore CNR di

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)

Prodotto

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Insieme di parole chiave di

• Parole chiave di "On-the-fly PCTL fast mean-field model-checking for self-organising coordination - Preliminary version" (Insieme di parole chiave)