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.
This work is partially supported by the EU project QUANTICOL (nr. 600708), and the IT MIUR project CINA
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-Checking Algorithms for Continuous Time Markov Chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003). IEEE CS
Benaïm, M., Le Boudec, J.: A class of mean field interaction models for computer and communication systems. Performance Evaluation 65(11–12), 823–838 (2008)
Bortolussi, L., Hillston, J.: Fluid model checking. CoRR abs/1203.0920 (2012), version 2, January 2013
Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012)
Bortolussi, L., Hillston, J.: Checking individual agent behaviours in markov population models by fluid approximation. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 113–149. Springer, Heidelberg (2013)
Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: A tutorial. Performance Evaluation 70(5), 317–349 (2013)
Darling, R., Norris, J.: Differential equation approximations for Markov chains. Probability Surveys 5, 37–79 (2008)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Bounded probabilistic model checking with the mur\({\varphi }\) verifier. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 214–229. Springer, Heidelberg (2004)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1994)
Hayden, R.: Scalable Performance Analysis of Massively Parallel Stochastic Systems. Ph.D. thesis, Imperial College London, April 2011. http://pubs.doc.ic.ac.uk/hayden-thesis/
Hillston, J.: Fluid flow approximation of PEPA models. In: Proceedings of the Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), pp. 33–43 (2005)
Kolesnichenko, A., de Boer, P.T., Remke, A., Haverkort, B.R.: A logic for model-checking mean-field models. In: DSN, pp. 1–12. IEEE (2013)
Kurtz, T.: Solutions of ordinary differential equations as limits of pure jump Markov processes. Journal of Applied Probability 7, 49–58 (1970)
Latella, D., Loreti, M., Massink, M.: On-the-fly fluid model checking via discrete time population models: Extended version. QUANTICOL TR-QC-08-2014 (2014). www.quanticol.eu
Latella, D., Loreti, M., Massink, M.: On-the-fly PCTL Fast Mean-Field Model-Checking for Self-organising Coordination. Science of Computer Programming. Elsevier (2015). http://dx.doi.org/10.1016/j.scico.2015.06.009
Latella, D., Loreti, M., Massink, M.: On-the-fly fast mean-field model-checking. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 297–314. Springer, Heidelberg (2014)
Latella, D., Loreti, M., Massink, M.: On-the-fly probabilistic model-checking. In: Proceedings 7th Interaction and Concurrency Experience ICE 2014. EPTCS, vol. 166 (2014)
Le Boudec, J.Y., McDonald, D., Mundinger, J.: A generic mean field convergence result for systems of interacting objects. In: QEST 2007, pp. 3–18. IEEE Computer Society Press (2007). ISBN: 978-0-7695-2883-0
LeVeque, R.J.: Finite Difference Methods for Ordinary and Partial Differential Equations. SIAM (2007)
Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Software Eng. 38(1), 205–219 (2012)
å Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: an empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46–60. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Latella, D., Loreti, M., Massink, M. (2015). On-the-fly Fluid Model Checking via Discrete Time Population Models. In: Beltrán, M., Knottenbelt, W., Bradley, J. (eds) Computer Performance Engineering. EPEW 2015. Lecture Notes in Computer Science(), vol 9272. Springer, Cham. https://doi.org/10.1007/978-3-319-23267-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-23267-6_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23266-9
Online ISBN: 978-3-319-23267-6
eBook Packages: Computer ScienceComputer Science (R0)