On-the-Fly Mean-Field Model-Checking for Attribute-Based Coordination
On-the-Fly Mean-Field Model-Checking for Attribute-Based Coordination
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.
Mean-field approximation, Difference and functional equations, Discrete time Markov chains, Markov processes, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Coordination Languages, PROBABILITY AND STATISTICS, Performance Analysis and Design Aids, Modes of Computation, Probabilistic model-checking, On-the-fly model-checking, Collective Adaptive Systems
Mean-field approximation, Difference and functional equations, Discrete time Markov chains, Markov processes, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Coordination Languages, PROBABILITY AND STATISTICS, Performance Analysis and Design Aids, Modes of Computation, Probabilistic model-checking, On-the-fly model-checking, Collective Adaptive Systems
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).4 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!