{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:36:33Z","timestamp":1767137793875,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319051185","type":"print"},{"value":"9783319051192","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05119-2_17","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T04:36:28Z","timestamp":1394166988000},"page":"297-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["On-the-fly Fast Mean-Field Model-Checking"],"prefix":"10.1007","author":[{"given":"Diego","family":"Latella","sequence":"first","affiliation":[]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"issue":"1","key":"17_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Trans. Comput. Logic 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"6","key":"17_CR2","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003). IEEE CS","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Bakhshi, R., Endrullis, J., Endrullis, S., Fokkink, W., Haverkort, B.: Automating the mean-field method for large dynamic gossip networks. In: QEST 2010, pp. 241\u2013250. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.38"},{"issue":"11\u201312","key":"17_CR4","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1016\/j.peva.2008.03.005","volume":"65","author":"M Bena\u00efm","year":"2008","unstructured":"Bena\u00efm, M., Le Boudec, J.Y.: A class of mean field interaction models for computer and communication systems. Perform. Eval. 65(11\u201312), 823\u2013838 (2008)","journal-title":"Perform. Eval."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL*. In: LICS, pp. 388\u2013397. IEEE Computer Society (1995)","DOI":"10.1109\/LICS.1995.523273"},{"key":"17_CR6","series-title":"LNCS","first-page":"333","volume-title":"CONCUR","author":"L Bortolussi","year":"2012","unstructured":"Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR. LNCS, vol. 7454, pp. 333\u2013347. Springer, Heidelberg (2012)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: a tutorial. Perform. Eval. 70(5), 317\u2013349 (2013). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0166531613000023","DOI":"10.1016\/j.peva.2013.01.001"},{"issue":"6","key":"17_CR8","doi-asserted-by":"publisher","first-page":"1013","DOI":"10.1016\/j.jcss.2007.07.005","volume":"74","author":"JT Bradley","year":"2008","unstructured":"Bradley, J.T., Gilmore, S.T., Hillston, J.: Analysing distributed internet worm attacks using continuous state-space approximation of process algebra models. J. Comput. Syst. Sci. 74(6), 1013\u20131032 (2008)","journal-title":"J. Comput. Syst. Sci."},{"key":"17_CR9","first-page":"109","volume-title":"SIGMETRICS\/Performance","author":"A Chaintreau","year":"2009","unstructured":"Chaintreau, A., Le Boudec, J.Y., Ristanovic, N.: The age of gossip: spatial mean field regime. In: Douceur, J.R., Greenberg, A.G., Bonald, T., Nieh, J. (eds.) SIGMETRICS\/Performance, pp. 109\u2013120. ACM, Seattle (2009)"},{"issue":"2","key":"17_CR10","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2\u20133","key":"17_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1(2\u20133), 275\u2013288 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1214\/07-PS121","volume":"5","author":"R Darling","year":"2008","unstructured":"Darling, R., Norris, J.: Differential equation approximations for Markov chains. Probab. Surv. 5, 37\u201379 (2008)","journal-title":"Probab. Surv."},{"key":"17_CR13","series-title":"LNCS","first-page":"214","volume-title":"FMCAD 2004","author":"G Della Penna","year":"2004","unstructured":"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\u2013229. Springer, Heidelberg (2004)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Gast, N., Gaujal, B.: A mean field model of work stealing in large-scale systems. In: Misra, V., Barford, P., Squillante, M.S. (eds.) SIGMETRICS. pp. 13\u201324. ACM (2010)","DOI":"10.1145\/1811099.1811042"},{"key":"17_CR15","series-title":"LNCS","first-page":"390","volume-title":"SENSORIA","author":"S Gnesi","year":"2011","unstructured":"Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Wirsing, M., H\u00f6lzl, M. (eds.) SENSORIA. LNCS, vol. 6582, pp. 390\u2013407. Springer, Heidelberg (2011)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Guirado, G., H\u00e9rault, T., Lassaigne, R., Peyronnet, S.: Distribution, approximation and probabilistic model checking. Electr. Notes Theor. Comput. Sci. 135(2), 19\u201330 (2006). http:\/\/dx.doi.org\/10.1016\/j.entcs.2005.10.016","DOI":"10.1016\/j.entcs.2005.10.016"},{"key":"17_CR17","series-title":"LNCS","first-page":"641","volume-title":"CAV 2009","author":"EM Hahn","year":"2009","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: INFAMY: an infinite-state Markov model checker. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 641\u2013647. Springer, Heidelberg (2009)"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6, 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"17_CR19","series-title":"LNCS","first-page":"73","volume-title":"VMCAI 2004","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"17_CR20","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Kolesnichenko, A., Remke, A., de Boer, P.T.: A logic for model-checking of mean-field models. Technical report TR-CTIT-12-11. http:\/\/doc.utwente.nl\/80267\/ (2012)","DOI":"10.1109\/DSN.2013.6575345"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Kolesnichenko, A., Remke, A., de Boer, P.T.: A logic for model-checking of mean-field models. In: Dependable Systems and Networks DSN13 (2013)","DOI":"10.1109\/DSN.2013.6575345"},{"issue":"2","key":"17_CR23","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking using PRISM: a Hybrid approach. STTT 6(2), 128\u2013142 (2004)","journal-title":"STTT"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Latella, D., Loreti, M., Massink, M.: On-the-fly fast mean-field model-checking: full version. Technical report. http:\/\/arxiv.org\/abs\/1312.3416 (2013)","DOI":"10.1007\/978-3-319-14128-2_17"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Latella, D., Loreti, M., Massink, M.: On-the-fly probabilistic model-checking: full version. Technical report. http:\/\/goo.gl\/uVkPP6\/ (2013)","DOI":"10.1007\/978-3-319-14128-2_17"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Le Boudec, J.Y., McDonald, D., Mundinger, J.: A generic mean field convergence result for systems of interacting objects. In: QEST07. pp. 3\u201318. IEEE Computer Society Press (2007). ISBN 978-0-7695-2883-0","DOI":"10.1109\/QEST.2007.8"},{"issue":"17","key":"17_CR27","doi-asserted-by":"publisher","first-page":"1557","DOI":"10.1016\/j.tcs.2010.09.024","volume":"412","author":"C McCaig","year":"2011","unstructured":"McCaig, C., Norman, R., Shankland, C.: From individuals to populations: a mean field semantics for process algebra. Theor. Comput. Sci. 412(17), 1557\u20131580 (2011)","journal-title":"Theor. Comput. Sci."},{"issue":"3\u20134","key":"17_CR28","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s11721-011-0062-z","volume":"5","author":"M.A. Montes de Oca","year":"2011","unstructured":"Montes de Oca, M.A., Ferrante, E., Scheidler, A., Pinciroli, C., Birattari, M., Dorigo, M.: Majority-rule opinion dynamics with differential latency: a mechanism for self-organized collective decision-making. Swarm Intell. 5(3\u20134), 305\u2013327 (2011)","journal-title":"Swarm Intell."},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Stefanek, A., Hayden, R.A., Bradley, J.T.: A new tool for the performance analysis of massively parallel computer systems. In: QAPL 2010. EPTCS, vol. 28. pp. 159\u2013181 (2010)","DOI":"10.4204\/EPTCS.28.11"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05119-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T20:35:58Z","timestamp":1746131758000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05119-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319051185","9783319051192"],"references-count":29,"aliases":["10.1007\/978-3-319-14128-2_17"],"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05119-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}