Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination. In: Science of Computer Programming, vol. 110 pp. 23 - 50. Elsevier, 2015. [Online First 27 June 2015]
Typical self-organising collective systems consist of a large number of interacting 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. We present a novel scalable, on-the-fly approximated model-checking procedure to verify bounded PCTL properties of selected individuals in the context of very large systems of independent 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 self-organising collective systems and an overview of remaining open issues and future extensions is provided.
URL: http://www.sciencedirect.com/science/article/pii/S016764231500132X
DOI: 10.1016/j.scico.2015.06.009
Subject Probabilistic model-checking
On-the-fly model-checking
Mean-field approximation
Discrete time Markov chains
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
F.1.2 Modes of Computation
F.1.1 Models of Computation
F.3.1 Specifying and Verifying and Reasoning about Programs
39-XX Difference and functional equations
60Jxx Markov processes

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional