PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Massink M. Design and optimisation of the FlyFast front-end for attribute-based coordination. In: QAPL 2017 - Quantitative Aspects of Programming Languages and Systems (Uppsala, Sweden, 23 aprile 2017). Proceedings, pp. 92 - 110. Herbert Wiklicky, Erik de Vink (eds.). (Electronic Proceedings in Theoretical Computer Science, vol. 250). Open Publishing Association, 2017.
 
 
Abstract
(English)
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.
URL: http://eptcs.web.cse.unsw.edu.au/paper.cgi?QAPL17.6
DOI: 10.4204/EPTCS.250.6
Subject Collective Adaptive Systems
Probabilistic model-checking
On-the-fly model-checking
Mean-field approximation
Discrete time Markov chains
Bisimilarity
B.8.2 PERFORMANCE AND RELIABILITY. Performance Analysis and Design Aids
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification
F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs
G.3 PROBABILITY AND STATISTICS
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