Design and Optimisation of the FlyFast Front-end for Attribute-based Coordination

Diego Latella
(Consiglio Nazionale delle Ricerche - Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo")
Mieke Massink
(Consiglio Nazionale delle Ricerche - Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo")

Collective Adaptive Systems (CAS) consist of a large number of interacting objects. The design of such systems requires scalable analysis tools and methods, which have necessarily to rely on some form of approximation of the system's actual behaviour. Promising techniques are those based on mean-field approximation. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individual(s) in the context of very large populations whose global behaviour is approximated using deterministic limit mean-field techniques. Recently, a front-end for FlyFast has been proposed which provides a modelling language, PiFF in the sequel, for the Predicate-based Interaction for FlyFast. In this paper we present details of PiFF design and an approach to state-space reduction based on probabilistic bisimulation for inhomogeneous DTMCs.

In Herbert Wiklicky and Erik de Vink: Proceedings 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2017), Uppsala, Sweden, 23rd April 2017, Electronic Proceedings in Theoretical Computer Science 250, pp. 92–110.
Published: 12th July 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.250.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org