Document - On-the-fly mean-field model-checking for attribute-based coordination

2016

Conference article Open Access

On-the-fly mean-field model-checking for attribute-based coordination

Ciancia V., Latella D., Massink M.

Difference and functional equations Mean-field approximation Modes of Computation Coordination Languages On-the-fly model-checking Specifying and Verifying and Reasoning about Programs Probabilistic model-checking Probabilistic on-the-fly model-checking [INFO]Computer Science [cs] Software/Program Verification Collective Adaptive Systems [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Discrete time Markov chains Markov processes Performance Analysis and Design Aids PROBABILITY AND STATISTICS

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.

Source: COORDINATION 2016 - DisCoTec 2016 - Coordination Models and Languages. 18th IFIP WG 6.1 International Conference, pp. 67–83, Heraklion, Crete, Greece, 6-9 June 2016

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:355159,
	title = {On-the-fly mean-field model-checking for attribute-based coordination},
	author = {Ciancia V. and Latella D. and Massink M.},
	doi = {10.1007/978-3-319-39519-7_5},
	booktitle = {COORDINATION 2016 - DisCoTec 2016 - Coordination Models and Languages. 18th IFIP WG 6.1 International Conference, pp. 67–83, Heraklion, Crete, Greece, 6-9 June 2016},
	year = {2016}
}