On-the-fly mean-field model-checking for attribute-based coordination preliminary version. Quanticol technical report TR-QC-01-2016

Ciancia V., Latella D., Massink M.

Collective adaptive systems  Probabilistic model-checking  On-the-fly model-checking  Mean-field approximation  Discrete time Markov chains 

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. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean- Field Approximated Model-checking. In particular, 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 a simple non value-passing version of 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 presented and proved correct. Application examples are also provided.

Source: ISTI Technical reports, 2016