{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:29:42Z","timestamp":1759336182076},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_9","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"147-163","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Safety Verification of Continuous-Space Pure Jump Markov Processes"],"prefix":"10.1007","author":[{"given":"Sadegh","family":"Esmaeil Zadeh Soudjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"6","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J.-P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 6, 624\u2013641 (2010)","journal-title":"Eur. J. Control"},{"issue":"11","key":"9_CR2","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"issue":"2","key":"9_CR3","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1111\/1468-0262.t01-1-00416","volume":"71","author":"Y A\u00eft-Sahalia","year":"2003","unstructured":"A\u00eft-Sahalia, Y., Mykland, P.A.: The effects of random and discrete sampling when estimating continuous-time diffusions. Econometrica 71(2), 483\u2013549 (2003)","journal-title":"Econometrica"},{"key":"9_CR4","volume-title":"An Introduction to Stochastic Processes with Applications to Biology","author":"LJS Allen","year":"2003","unstructured":"Allen, L.J.S.: An Introduction to Stochastic Processes with Applications to Biology. Pearson\/Prentice Hall, Englewood Cliffs (2003)"},{"key":"9_CR5","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. 1102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"key":"9_CR6","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: Allen Emerson, E., Prasad Sistla, A. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358\u2013372. Springer, Heidelberg (2000)"},{"issue":"6","key":"9_CR7","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)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains (extended abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146\u2013161. Springer, Heidelberg (1999)"},{"key":"9_CR10","volume-title":"Stchastic Optimal Control: the Discrete-Time Case","author":"DP Bertsekas","year":"1996","unstructured":"Bertsekas, D.P., Shreve, S.E.: Stchastic Optimal Control: the Discrete-Time Case. Athena Scientific, Belmont (1996)"},{"key":"9_CR11","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316962","volume-title":"Convergence of Probability Measures","author":"P Billingsley","year":"1999","unstructured":"Billingsley, P.: Convergence of Probability Measures. Wiley, New York (1999)"},{"issue":"5","key":"9_CR12","doi-asserted-by":"publisher","first-page":"1389","DOI":"10.1016\/j.enconman.2008.12.012","volume":"50","author":"DS Callaway","year":"2009","unstructured":"Callaway, D.S.: Tapping the energy storage potential in electric loads to deliver load following and regulation, with application to wind energy. Ener. Convers. Manag. 50(5), 1389\u20131400 (2009)","journal-title":"Ener. Convers. Manag."},{"key":"9_CR13","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. 6919, pp. 26\u201342. Springer, Heidelberg (2011)"},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(1:12)2011","volume":"7","author":"T Chen","year":"2011","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods Comput. Sci. 7(1), 1\u201334 (2011)","journal-title":"Logical Methods Comput. Sci."},{"key":"9_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-4483-2","volume-title":"Markov Models and Optimization","author":"MHA Davis","year":"1993","unstructured":"Davis, M.H.A.: Markov Models and Optimization. Chapman & Hall\/CRC Press, London (1993)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive gridding for abstraction and verification of stochastic hybrid systems. In: QEST, pp. 59\u201369 (2011)","DOI":"10.1109\/QEST.2011.16"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-642-33386-6_32","volume-title":"Automated Technology for Verification and Analysis","author":"S Esmaeil Zadeh Soudjani","year":"2012","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Higher-order approximations for verification of stochastic hybrid systems. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 416\u2013434. Springer, Heidelberg (2012)"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S Esmaeil Zadeh Soudjani","year":"2013","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2013)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-54862-8_45","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Esmaeil Zadeh Soudjani","year":"2014","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Precise approximations of the probability distribution of a Markov process in time: an application to probabilistic invariance. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 547\u2013561. Springer, Heidelberg (2014)"},{"issue":"3","key":"9_CR20","doi-asserted-by":"publisher","first-page":"975","DOI":"10.1109\/TCST.2014.2358844","volume":"23","author":"S Esmaeil Zadeh Soudjani","year":"2015","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Aggregation and control of populations of thermostatically controlled loads by formal abstractions. IEEE Trans. Control Syst. Technol. 23(3), 975\u2013990 (2015)","journal-title":"IEEE Trans. Control Syst. Technol."},{"issue":"3","key":"9_CR21","first-page":"1","volume":"11","author":"SEZ Soudjani","year":"2015","unstructured":"Soudjani, S.E.Z., Abate, A.: Quantitative approximation of the probability distribution of a Markov process by formal abstractions. Logical Methods Comput. Sci 11(3), 1\u201329 (2015)","journal-title":"Logical Methods Comput. Sci"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-3-662-46681-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Esmaeil Zadeh Soudjani","year":"2015","unstructured":"Esmaeil Zadeh Soudjani, S., Gevaerts, C., Abate, A.: \n                      \n                        \n                      \n                      $${\\sf FAUST^2}$$\n                    : formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tineli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272\u2013286. Springer, Heidelberg (2015)"},{"key":"9_CR23","series-title":"Die Grundlehren der mathematischen Wissenschaften","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61921-2","volume-title":"The Theory of Stochastic Processes: II","author":"II Gihman","year":"1975","unstructured":"Gihman, I.I., Skorokhod, A.V.: The Theory of Stochastic Processes: II. Die Grundlehren der mathematischen Wissenschaften, vol. 218. Springer, Heidelberg (1975)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"9_CR25","series-title":"Grundlehren der mathematischen Wissenschaften","volume-title":"Limit Theorems for Stochastic Processes","author":"J Jacod","year":"2010","unstructured":"Jacod, J., Shiryaev, A.: Limit Theorems for Stochastic Processes. Grundlehren der mathematischen Wissenschaften. Springer, Heidelberg (2010)"},{"key":"9_CR26","series-title":"Probability and its Applications","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4015-8","volume-title":"Foundations of Modern Probability","author":"O Kallenberg","year":"2002","unstructured":"Kallenberg, O.: Foundations of Modern Probability. Probability and its Applications. Springer, New York (2002)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243\u2013244. IEEE (2005)","DOI":"10.1109\/QEST.2005.2"},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1109\/TPWRS.2012.2204074","volume":"28","author":"JL Mathieu","year":"2013","unstructured":"Mathieu, J.L., Koch, S., Callaway, D.S.: State estimation and control of electric loads to manage real-time energy imbalance. IEEE Trans. Power Syst. 28(1), 430\u2013440 (2013)","journal-title":"IEEE Trans. Power Syst."},{"key":"9_CR29","unstructured":"Micheli, M., Jordan, M.: Random sampling of a continuous-time stochastic dynamical system. In: Proceedings of the 15th International Symposium on the Mathematical Theory of Networks and Systems (MTNS), pp. 1\u201315 (2002)"},{"key":"9_CR30","doi-asserted-by":"publisher","DOI":"10.1142\/9781848162891","volume-title":"Labelled Markov Processes","author":"P Panangaden","year":"2009","unstructured":"Panangaden, P.: Labelled Markov Processes. Imperial College Press, London (2009)"},{"key":"9_CR31","series-title":"Stochastic Modelling and Applied Probability","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13694-8","volume-title":"Numerical Solution of Stochastic Differential Equations with Jumps in Finance","author":"E Platen","year":"2010","unstructured":"Platen, E., Bruti-Liberati, N.: Numerical Solution of Stochastic Differential Equations with Jumps in Finance. Stochastic Modelling and Applied Probability. Springer, Heidelberg (2010)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: On infinite-horizon probabilistic properties and stochastic bisimulation functions. In: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, pp. 526\u2013531, Orlando, FL, December 2011","DOI":"10.1109\/CDC.2011.6160617"},{"key":"9_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.09.032","volume":"515","author":"I Tkachev","year":"2014","unstructured":"Tkachev, I., Abate, A.: Characterization and computation of infinite-horizon specifications over Markov processes. Theor. Comput. Sci. 515, 1\u201318 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR34","series-title":"North-Holland Personal Library","volume-title":"Stochastic Processes in Physics and Chemistry","author":"NG Kampen Van","year":"2011","unstructured":"Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry. North-Holland Personal Library. Elsevier Science, Amsterdam (2011)"},{"key":"9_CR35","unstructured":"Ziai, Y.: Statistical models of claim amount distributions in general insurance. Ph.D. thesis, School of Engineering and Maths, City University London (1979)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:13:02Z","timestamp":1585012382000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}