We show that, under suitable convergence and scaling conditions, fluid model checking bounded CSL formulas on selected individuals in a continuous large population model can be approximated by checking equivalent bounded PCTL formulas on corresponding objects in a discrete time, time synchronous Markov population model, using an on-the-fly mean field approach. The proposed technique is applied to a benchmark epidemic model and a client-server case study showing promising results also for the challenging case of nested formulas with time dependent truth values. The on-the-fly results are compared to those obtained via global fluid model checking and statistical model-checking.
On-the-fly fluid model checking via discrete time population models / Latella, Diego; Loreti, Michele; Massink, Mieke. - STAMPA. - (2015), pp. 193-207. [10.1007/978-3-319-23267-6_13]
On-the-fly fluid model checking via discrete time population models
LORETI, MICHELE;MASSINK, MIEKE
2015
Abstract
We show that, under suitable convergence and scaling conditions, fluid model checking bounded CSL formulas on selected individuals in a continuous large population model can be approximated by checking equivalent bounded PCTL formulas on corresponding objects in a discrete time, time synchronous Markov population model, using an on-the-fly mean field approach. The proposed technique is applied to a benchmark epidemic model and a client-server case study showing promising results also for the challenging case of nested formulas with time dependent truth values. The on-the-fly results are compared to those obtained via global fluid model checking and statistical model-checking.I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.