RESULTS FROM 1 TO 1 OF 1

2017, Contributo in volume, ENG

FlyFast: a scalable approach to probabilistic model-checking based on mean-field approximation

Latella D.; Loreti M.; Massink M.

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.

DOI: 10.1007/978-3-319-68270-9_13

InstituteSelected 0/1
    ISTI, Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo" (1)
AuthorSelected 0/2
    Latella Diego (1)
    Massink Mieke (1)
TypeSelected 0/1
    Contributo in volume (1)
Research programSelected 0/0
No values ​​available
EU Funding ProgramSelected 0/1
    FP7 (1)
EU ProjectSelected 0/1
    QUANTICOL (1)
YearSelected 0/1
    2017 (1)
LanguageSelected 0/1
    Inglese (1)
Keyword

Probabilistic on-the-fly model-checking

RESULTS FROM 1 TO 1 OF 1