{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:26Z","timestamp":1760202686308,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319229744"},{"type":"electronic","value":"9783319229751"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-22975-1_12","type":"book-chapter","created":{"date-parts":[[2015,8,21]],"date-time":"2015-08-21T08:37:43Z","timestamp":1440146263000},"page":"172-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Fluid Model Checking of Timed Properties"],"prefix":"10.1007","author":[{"given":"Luca","family":"Bortolussi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberta","family":"Lanciani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,22]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A Theory of Timed Automata. Theor. Comput. Sci. (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"12_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1158-7","volume-title":"Stochastic Epidemic Models and their Statistical Analysis","author":"H Andersson","year":"2000","unstructured":"Andersson, H., Britton, T.: Stochastic Epidemic Models and their Statistical Analysis. Springer, New York (2000)"},{"key":"12_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press (2008)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-642-19835-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Barbot","year":"2011","unstructured":"Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128\u2013142. Springer, Heidelberg (2011)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Benaim, M., Le Boudec, J.-Y.: A class of mean field interaction models for computer and communication systems. Perform. Evaluation (2008)","DOI":"10.4108\/ICST.WIOPT2008.3117"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J.: Fluid approximation of CTMC with deterministic delays. In: Proceedings of QEST (2012)","DOI":"10.1109\/QEST.2012.13"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J.: Efficient checking of individual rewards properties in Markov population models. In: Proceedings of QAPL (2015)","DOI":"10.4204\/EPTCS.194.3"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J.: Model Checking Single Agent Behaviours by Fluid Approximation. Inform. Comput. (2015)","DOI":"10.1016\/j.ic.2015.03.002"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous Approximation of Collective Systems Behaviour: a Tutorial. Perform. Evaluation (2013)","DOI":"10.1016\/j.peva.2013.01.001"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-40196-1_9","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2013","unstructured":"Bortolussi, L., Lanciani, R.: Model checking Markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123\u2013138. Springer, Heidelberg (2013)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/978-3-319-10885-8_16","volume-title":"Computer Performance Engineering","author":"L Bortolussi","year":"2014","unstructured":"Bortolussi, L., Lanciani, R.: Stochastic approximation of global reachability probabilities of Markov population models. In: Horv\u00e1th, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 224\u2013239. Springer, Heidelberg (2014)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Verification of linear duration properties over CTMCs. Proceedings of TOCL (2013)","DOI":"10.1145\/2185632.2185672"},{"key":"12_CR13","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 (2011)","DOI":"10.2168\/LMCS-7(1:12)2011"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","first-page":"2","volume-title":"Reachability Problems","author":"T Chen","year":"2011","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Observing continuous-time MDPs by 1-clock timed automata. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 2\u201325. Springer, Heidelberg (2011)"},{"key":"12_CR15","unstructured":"Cinlar, E.: Introduction to Stochastic Processes. Courier Corporation (2013)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Darling, R., Norris, J., et al.: Differential Equation Approximations for Markov Chains. Probability Surveys (2008)","DOI":"10.1214\/07-PS121"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model Checking Timed and Stochastic Properties with $$\\text{ CSL }^{TA}$$. IEEE Trans. Software Eng. (2009)","DOI":"10.1109\/TSE.2008.108"},{"key":"12_CR18","unstructured":"Ethier, S.N., Kurtz, T.G.: Markov Processes: Characterization and Convergence. Wiley (2005)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Fu, H.: Approximating acceptance probabilities of ctmc-paths on multi-clock deterministic timed automata. In: Proceedings of HSCC (2013)","DOI":"10.1145\/2461328.2461376"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Gast, N., Bruno, G.: A Mean Field Model of Work Stealing in Large-Scale Systems. ACM SIGMETRICS Performance Evaluation Review (2010)","DOI":"10.1145\/1811039.1811042"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Guglielmi, N., Hairer, E.: Implementing Radau IIA Methods for Stiff Delay Differential Equations. Computing (2001)","DOI":"10.1007\/s006070170013"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Hayden, R.A.: Mean field for performance models with deterministically-timed transitions. In: Proceedings of QEST (2012)","DOI":"10.1109\/QEST.2012.27"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Hayden, R.A., Bradley, J.T., Clark, A.: Performance Specification and Evaluation with Unified Stochastic Probes and Fluid Analysis. IEEE Trans. Software Eng. (2013)","DOI":"10.1109\/TSE.2012.1"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-3-319-05119-2_17","volume-title":"Trustworthy Global Computing","author":"D Latella","year":"2014","unstructured":"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\u2013314. Springer, Heidelberg (2014)"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/3-540-46429-8_14","volume-title":"Computer Performance Evaluation. Modelling Techniques and Tools","author":"A Zimmermann","year":"2000","unstructured":"Zimmermann, A., Freiheit, J., German, R., Hommel, G.: Petri net modelling and performability evaluation with timeNET 3.0. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol. 1786, p. 188. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22975-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T07:33:25Z","timestamp":1676964805000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22975-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319229744","9783319229751"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22975-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"22 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}