{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:38Z","timestamp":1760202638822,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642388736"},{"type":"electronic","value":"9783642388743"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38874-3_4","type":"book-chapter","created":{"date-parts":[[2013,6,9]],"date-time":"2013-06-09T22:11:59Z","timestamp":1370815919000},"page":"113-149","source":"Crossref","is-referenced-by-count":5,"title":["Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation"],"prefix":"10.1007","author":[{"given":"Luca","family":"Bortolussi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jane","family":"Hillston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"GNU Octave"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1016\/S0377-0427(00)00342-3","volume":"121","author":"G. Alefeld","year":"2000","unstructured":"Alefeld, G., Mayer, G.: Interval analysis: theory and applications. Journal of Computational and Applied Mathematics\u00a0121, 421\u2013464 (2000)","journal-title":"Journal of Computational and Applied Mathematics"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Andreychenko, A., Crouzen, P., Wolf, V.: On-the-fly uniformization of time-inhomogeneous infinite Markov population models. In: Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages, QAPL 2011. EPTCS, vol.\u00a057, p. 1 (2011)","DOI":"10.4204\/EPTCS.57.1"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"key":"4_CR5","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)"},{"issue":"4","key":"4_CR6","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C. Baier","year":"2007","unstructured":"Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Software Eng.\u00a033(4), 209\u2013224 (2007)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR7","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 the Sixth International Conference on the Quantitative Evaluation of Systems, QEST 2009, pp. 247\u2013256. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.38"},{"issue":"2","key":"4_CR8","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.peva.2010.08.025","volume":"68","author":"R. Bakhshi","year":"2011","unstructured":"Bakhshi, R., Cloth, L., Fokkink, W., Haverkort, B.R.: Mean-field framework for performance evaluation of push-pull gossip protocols. Perform. Eval.\u00a068(2), 157\u2013179 (2011)","journal-title":"Perform. Eval."},{"key":"4_CR9","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":"4_CR10","unstructured":"Bena\u00efm, M., Le Boudec, J.Y.: On mean field convergence and stationary regime. CoRR, abs\/1111.5710 (2011)"},{"issue":"1-2","key":"4_CR11","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0304-3800(01)00463-X","volume":"150","author":"L. Berec","year":"2002","unstructured":"Berec, L.: Techniques of spatially explicit individual-based models: construction, simulation, and mean-field analysis. Ecological Modelling\u00a0150(1-2), 55\u201381 (2002)","journal-title":"Ecological Modelling"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-32940-1_24","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"L. Bortolussi","year":"2012","unstructured":"Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 333\u2013347. Springer, Heidelberg (2012)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J.: Fluid model checking. CoRR, 1203.0920 (2012)","DOI":"10.1007\/978-3-642-32940-1_24"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: a tutorial. Performance Evaluation (2013)","DOI":"10.1016\/j.peva.2013.01.001"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Bortolussi, L.: On the approximation of stochastic concurrent constraint programming by master equation, vol.\u00a0220, pp. 163\u2013180 (2008)","DOI":"10.1016\/j.entcs.2008.11.025"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-642-04186-0_11","volume-title":"Transactions on Computational Systems Biology XI","author":"L. Bortolussi","year":"2009","unstructured":"Bortolussi, L., Policriti, A.: Dynamical systems and stochastic programming: To ordinary differential equations and back. In: Priami, C., Back, R.-J., Petre, I. (eds.) Transactions on Computational Systems Biology XI. LNCS, vol.\u00a05750, pp. 216\u2013267. Springer, Heidelberg (2009)"},{"key":"4_CR17","unstructured":"Burden, R.L., Faires, J.D.: Numerical analysis. Thomson Brooks\/Cole (2005)"},{"key":"4_CR18","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":"4_CR19","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science 7(1) (2011)","DOI":"10.2168\/LMCS-7(1:12)2011"},{"key":"4_CR20","unstructured":"Clarke, E., Peled, A., Grunberg, A.: Model Checking. MIT Press (1999)"},{"key":"4_CR21","unstructured":"Darling, R.W.R.: Fluid limits of pure jump Markov processes: A practical guide (2002), \n                  \n                    http:\/\/arXiv.org"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Darling, R.W.R., Norris, J.R.: Differential equation approximations for Markov chains. Probability Surveys 5 (2008)","DOI":"10.1214\/07-PS121"},{"issue":"2","key":"4_CR23","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S. Donatelli","year":"2009","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL\n                  TA\n                . IEEE Trans. Software Eng.\u00a035(2), 224\u2013240 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR24","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"},{"issue":"1","key":"4_CR25","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."},{"issue":"1","key":"4_CR26","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/TSE.2012.1","volume":"39","author":"R.A. Hayden","year":"2013","unstructured":"Hayden, R.A., Bradley, J.T., Clark, A.: Performance specification and evaluation with unified stochastic probes and fluid analysis. IEEE Trans. Software Eng.\u00a039(1), 97\u2013118 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Hillston, J.: Fluid flow approximation of PEPA models. In: Proceedings of the Second International Conference on the Quantitative Evaluation of SysTems, QEST 2005, pp. 33\u201342 (September 2005)","DOI":"10.1109\/QEST.2005.12"},{"key":"4_CR28","unstructured":"Jensen, A.: Markov chains as an aid in the study of Markov processes. Skandinavisk Aktuarietidskriff 36 (1953)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"S.K. Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol.\u00a05688, pp. 218\u2013234. Springer, Heidelberg (2009)"},{"key":"4_CR30","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)"},{"key":"4_CR31","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":"4_CR32","doi-asserted-by":"crossref","unstructured":"Kolesnichenko, A., Remke, A., de Boer, P.-T., Haverkort, B.R.: A logic for model-checking of mean-field models. In: Proceedings of the 43rd International Conference on Dependable Systems and Networks, DSN 2013 (2013)","DOI":"10.1109\/DSN.2013.6575345"},{"key":"4_CR33","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":"4_CR34","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1017\/S0021900200026929","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"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Kurtz, T.G.: Approximation of population processes. SIAM (1981)","DOI":"10.1137\/1.9781611970333"},{"issue":"2","key":"4_CR36","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 with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer\u00a06(2), 128\u2013142 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"4_CR38","volume-title":"Performance Evaluation of Computer and Communication Systems","author":"J.-Y. Boudec Le","year":"2010","unstructured":"Le Boudec, J.-Y.: Performance Evaluation of Computer and Communication Systems. EPFL Press, Lausanne (2010)"},{"issue":"2","key":"4_CR39","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-011-0188-1","volume":"24","author":"M. Massink","year":"2012","unstructured":"Massink, M., Latella, D., Bracciali, A., Harrison, M., Hillston, J.: Scalable context-dependent analysis of emergency egress models. Formal Aspects of Computing\u00a024(2), 267\u2013302 (2012)","journal-title":"Formal Aspects of Computing"},{"key":"4_CR40","unstructured":"MATLAB: v. 7.10.0 (R2010a). The MathWorks Inc., Natick, Massachusetts (2010)"},{"key":"4_CR41","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":"4_CR42","doi-asserted-by":"crossref","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511810633"},{"key":"4_CR43","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/S0301-4622(02)00145-X","volume":"101","author":"H. Qian","year":"2002","unstructured":"Qian, H., Elson, E.L.: Single-molecule enzymology: stochastic michaelis-menten kinetics. Biophysical Chemistry\u00a0101, 565\u2013576 (2002)","journal-title":"Biophysical Chemistry"},{"issue":"1","key":"4_CR44","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":"4_CR45","doi-asserted-by":"crossref","unstructured":"Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, vol.\u00a023. American Mathematical Society (2004)","DOI":"10.1090\/crmm\/023"},{"key":"4_CR46","unstructured":"Sumpter, D.T.J.: From Bee to Society: An Agent-based Investigation of Honey Bee Colonies. PhD thesis, University of Manchester (2000)"},{"key":"4_CR47","unstructured":"Szallasi, Z., Stelling, J., Periwal, V. (eds.): System Modeling in Cellular Biology, From Concepts to Nuts and Bolts. MIT Press (2012)"},{"issue":"4","key":"4_CR48","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1109\/TSE.2011.81","volume":"38","author":"M. Tribastone","year":"2012","unstructured":"Tribastone, M., Ding, J., Gilmore, S., Hillston, J.: Fluid rewards for a stochastic process algebra. IEEE Trans. Software Eng.\u00a038(4), 861\u2013874 (2012)","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"4_CR49","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/TSE.2010.82","volume":"38","author":"M. Tribastone","year":"2012","unstructured":"Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Software Eng.\u00a038(1), 205\u2013219 (2012)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR50","unstructured":"Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry. Elsevier (1992)"},{"key":"4_CR51","unstructured":"van Moorsel, A.P.A., Wolter, K.: Numerical solution of non-homogeneous Markov processes through uniformization. In: Proceedings of the 12th European Simulation Multiconference - Simulation- Past, Present and Future, ESM 1998, pp. 710\u2013717. SCS Europe (1998)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Dynamical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38874-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:54:19Z","timestamp":1558302859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38874-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388736","9783642388743"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38874-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}