{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T16:56:28Z","timestamp":1793033788147,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642329395","type":"print"},{"value":"9783642329401","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32940-1_24","type":"book-chapter","created":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T20:47:02Z","timestamp":1346532422000},"page":"333-347","source":"Crossref","is-referenced-by-count":34,"title":["Fluid Model Checking"],"prefix":"10.1007","author":[{"given":"Luca","family":"Bortolussi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jane","family":"Hillston","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Andreychenko, A., Crouzen, P., Wolf, V.: On-the-fly Uniformization of Time-Inhomogeneous Infinite Markov Population Models. In: Proceedings of QAPL 2011. ENTCS, vol.\u00a057, pp. 1\u201315 (2011)","DOI":"10.4204\/EPTCS.57.1"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model Checking Continuous-Time Markov Chains by Transient Analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 358\u2013372. Springer, Heidelberg (2000)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Bakhshi, R., Cloth, L., Fokkink, W., Haverkort, B.R.: Mean-field analysis for the evaluation of gossip protocols. In: Proceedings of QEST 2009, pp. 247\u2013256. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.38"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bena\u00efm, M., Le Boudec, J.: A class of mean field interaction models for computer and communication systems. Performance Evaluation (2008)","DOI":"10.4108\/ICST.WIOPT2008.3117"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Bobbio, A., Gribaudo, M., Telek, M.: Analysis of large scale interacting systems by mean field method. In: Proceedings of QEST 2008, pp. 215\u2013224. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.47"},{"key":"24_CR6","unstructured":"Bortolussi, L., Hillston, J.: Fluid model checking. CoRR 1203.0920 (2012), \n                    \n                      http:\/\/arxiv.org\/abs\/1203.0920"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Policriti, A.: Dynamical systems and stochastic programming \u2014 from ordinary differential equations and back. Trans. Comp. Sys. Bio.\u00a0XI (2009)","DOI":"10.1007\/978-3-642-04186-0_11"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-24310-3_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T. Chen","year":"2011","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-Bounded Verification of CTMCs against Real-Time Specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol.\u00a06919, pp. 26\u201342. Springer, Heidelberg (2011)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-04761-9_10","volume-title":"Automated Technology for Verification and Analysis","author":"T. Chen","year":"2009","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: LTL Model Checking of Time-Inhomogeneous Markov Chains. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 104\u2013119. Springer, Heidelberg (2009)"},{"key":"24_CR10","unstructured":"Darling, R.W.R.: Fluid limits of pure jump Markov processes: A practical guide (2002), \n                    \n                      http:\/\/arxiv.org\/abs\/math.PR\/0210109"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Darling, R.W.R., Norris, J.R.: Differential equation approximations for Markov chains. Probability Surveys\u00a05 (2008)","DOI":"10.1214\/07-PS121"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-22993-0_30","volume-title":"Mathematical Foundations of Computer Science 2011","author":"P. Franek","year":"2011","unstructured":"Franek, P., Ratschan, S., Zgliczynski, P.: Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol.\u00a06907, pp. 315\u2013326. Springer, Heidelberg (2011)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Gast, N., Gaujal, B.: A mean field model of work stealing in large-scale systems. In: Proceedings of ACM SIGMETRICS 2010, pp. 13\u201324 (2010)","DOI":"10.1145\/1811099.1811042"},{"key":"24_CR14","unstructured":"Hayden, R.A., Bradley, J.T., Clark, A.: Performance Specification and Evaluation with Unified Stochastic Probes and Fluid Analysis. IEEE Trans. Soft. Eng."},{"issue":"1","key":"24_CR15","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1016\/j.tcs.2011.07.017","volume":"413","author":"R.A. Hayden","year":"2012","unstructured":"Hayden, R.A., Stefanek, A., Bradley, J.T.: Fluid computation of passage-time distributions in large Markov models. Theor. Comput. Sci.\u00a0413(1), 106\u2013141 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Hillston, J.: Fluid flow approximation of PEPA models. In: Proceedings of QEST 2005, pp. 33\u201342. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.12"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-540-85778-5_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J.-P. Katoen","year":"2008","unstructured":"Katoen, J.-P., Mereacre, A.: Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 203\u2013217. Springer, Heidelberg (2008)"},{"issue":"3","key":"24_CR18","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2008.11.016","volume":"220","author":"M. Kattenbelt","year":"2008","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based probabilistic predicate abstraction in PRISM. Electr. Notes Theor. Comput. Sci.\u00a0220(3), 5\u201321 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-93900-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Kattenbelt","year":"2009","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction Refinement for Probabilistic Software. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 182\u2013197. Springer, Heidelberg (2009)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-24749-1_11","volume-title":"Computer Performance Engineering","author":"A. Kolesnichenko","year":"2011","unstructured":"Kolesnichenko, A., Remke, A., de Boer, P.-T., Haverkort, B.R.: Comparison of the Mean-Field Approach and Simulation in a Peer-to-Peer Botnet Case Study. In: Thomas, N. (ed.) EPEW 2011. LNCS, vol.\u00a06977, pp. 133\u2013147. Springer, Heidelberg (2011)"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Krantz, S., Harold, P.R.: A Primer of Real Analytic Functions, 2nd edn. Birkh\u00e4user (2002)","DOI":"10.1007\/978-0-8176-8134-0"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"49","DOI":"10.2307\/3212147","volume":"7","author":"T.G. Kurtz","year":"1970","unstructured":"Kurtz, T.G.: Solutions of ordinary differential equations as limits of pure jump Markov processes. Journal of Applied Probability\u00a07, 49\u201358 (1970)","journal-title":"Journal of Applied Probability"},{"issue":"2","key":"24_CR23","doi-asserted-by":"crossref","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 with PRISM: A hybrid approach. Int. Journal on Software Tools for Technology Transfer\u00a06(2), 128\u2013142 (2004)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"24_CR24","doi-asserted-by":"crossref","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 with PRISM: A hybrid approach. Int. Journal on Software Tools for Technology Transfer\u00a06(2), 128\u2013142 (2004)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"24_CR25","volume-title":"Interval Methods for Systems of Equations","author":"A. Neumaier","year":"1990","unstructured":"Neumaier, A.: Interval Methods for Systems of Equations. University Press, Cambridge (1990)"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511810633"},{"issue":"1","key":"24_CR27","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s11786-007-0002-x","volume":"1","author":"D. Richardson","year":"2007","unstructured":"Richardson, D.: Zero tests for constants in simple scientific computation. Mathematics in Computer Science\u00a01(1), 21\u201337 (2007)","journal-title":"Mathematics in Computer Science"},{"key":"24_CR28","unstructured":"Rudin, W.: Principles of Mathematical Analysis. McGraw-Hill (1976)"},{"issue":"5","key":"24_CR29","first-page":"1","volume":"2","author":"P. Taylor","year":"2010","unstructured":"Taylor, P.: A lambda calculus for real analysis. Journal of Logic and Analysis\u00a02(5), 1\u2013115 (2010)","journal-title":"Journal of Logic and Analysis"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2012 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32940-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:49:36Z","timestamp":1620128976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32940-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329395","9783642329401"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32940-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}