Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. FlyFast: a scalable approach to probabilistic model-checking based on mean-field approximation. Joost-Pieter Katoen, Rom Langerak, Arend Rensink (eds.). (Lecture Notes in Computer Science, vol. 10500). Cham, Switzerland: Springer, 2017.
Model-checking is an effective formal verification technique that has also been extended to quantitative logics and models such as PCTL and DTMCs as well as CSL and CTMCs/CTMDPs. Unfortunately, the state-space explosion problem of classical model-checking algorithms affects also quantitative extensions. Mean-field techniques provide approximations of the mean behaviour of large population models. These approximations are deterministic: a unique value of the fractions of agents in each state is computed for each time instant. A drastic reduction of the size of the model is obtained enabling the definition of an efficient model-checking algorithm. This paper is a survey of work we have done in the last few years in the area of mean-field approximated probabilistic model-checking. We start with a brief description of FlyFast, an on-the-fly model checker we have developed for approximated bounded PCTL model-checking, based on mean-field population DTMC approximation. Then we show an example of use of FlyFast in the context of Collective Adaptive Systems. We also discuss two additional interesting front-ends for FlyFast; the first one is a translation from CTMC-based population models and (a fragment of) CSL that allows for approximate probabilistic model-checking in the continuous stochastic time setting; the second one is a translation from a predicate-based process interaction language that allows for probabilistic model-checking of models based on components equipped both with behaviour and with attributes, on which predicates are defined that can be used in component interaction primitives.
URL: http://https://link.springer.com/chapter/10.1007/978-3-319-68270-9_13#aboutcontent
DOI: 10.1007/978-3-319-68270-9_13
Subject Probabilistic model-checking
On-the-fly model-checking
Mean-field approximation
Discrete time Markov chains
Software Tools
B.8.2 PERFORMANCE AND RELIABILITY. Performance Analysis and Design Aids
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification
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