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

Latella D., Loreti M., Massink M.

Probabilistic on-the-fly model-checking  Mean-field approximation  Time bounded probabilistic computation tree logic  Collective adaptive systems  Discrete time markov chains 

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.

Source: ModelEd,TestEd, TrustEd. Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday,, edited by J-P. Katoen, R. Langerak, A. Rensink, pp. 254–275. New York: Springer International Publishing, 2017

Publisher: Springer International Publishing, New York, USA

Metrics