On-the-Fly Mean-Field Model-Checking for Attribute-Based Coordination

Abstract : Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging, as it requires scalable analysis tools and methods to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is given and proved correct. Application examples are also provided.
Type de document :
Communication dans un congrès
Alberto Lluch Lafuente; José Proença. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. Springer International Publishing, Lecture Notes in Computer Science, LNCS-9686, pp.67-83, 2016, Coordination Models and Languages. 〈10.1007/978-3-319-39519-7_5〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01631720
Contributeur : Hal Ifip <>
Soumis le : jeudi 9 novembre 2017 - 16:13:59
Dernière modification le : mercredi 20 décembre 2017 - 17:38:25
Document(s) archivé(s) le : samedi 10 février 2018 - 15:04:20

Fichier

 Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Vincenzo Ciancia, Diego Latella, Mieke Massink. On-the-Fly Mean-Field Model-Checking for Attribute-Based Coordination. Alberto Lluch Lafuente; José Proença. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. Springer International Publishing, Lecture Notes in Computer Science, LNCS-9686, pp.67-83, 2016, Coordination Models and Languages. 〈10.1007/978-3-319-39519-7_5〉. 〈hal-01631720〉

Partager

Métriques

Consultations de la notice

27