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.
CITATION STYLE
Latella, D., Loreti, M., & Massink, M. (2015). On-the-fly fluid model checking via discrete time population models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9272, pp. 193–207). Springer Verlag. https://doi.org/10.1007/978-3-319-23267-6_13
Mendeley helps you to discover research relevant for your work.