{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T13:47:36Z","timestamp":1762004856671},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319542911"},{"type":"electronic","value":"9783319542928"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-54292-8_1","type":"book-chapter","created":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T02:12:49Z","timestamp":1487211169000},"page":"1-14","source":"Crossref","is-referenced-by-count":2,"title":["Verification of Networks of Smart Energy Systems over the Cloud"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,17]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2013.12.002","volume":"297","author":"A Abate","year":"2012","unstructured":"Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. Electron. Notes Theor. Comput. Sci. 297, 3\u201325 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"11","key":"1_CR2","doi-asserted-by":"crossref","first-page":"2688","DOI":"10.1109\/TAC.2011.2160595","volume":"56","author":"A Abate","year":"2011","unstructured":"Abate, A., D\u2019Innocenzo, A., Di Benedetto, M.D.: Approximate abstractions of stochastic hybrid systems. IEEE Trans. Autom. Control 56(11), 2688\u20132694 (2011)","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR3","doi-asserted-by":"crossref","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"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-319-06880-0_2","volume-title":"Horizons of the Mind. A Tribute to Prakash Panangaden","author":"A Abate","year":"2014","unstructured":"Abate, A., Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking of labelled markov processes via finite approximate bisimulations. In: Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 40\u201358. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-06880-0_2"},{"issue":"11","key":"1_CR5","doi-asserted-by":"crossref","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"},{"key":"1_CR6","unstructured":"Various authors. FP7 AMBI project. http:\/\/www.ambi-project.eu"},{"key":"1_CR7","unstructured":"Various authors. FP7 MoVeS project. http:\/\/www.movesproject.eu"},{"issue":"9","key":"1_CR8","doi-asserted-by":"crossref","first-page":"2665","DOI":"10.1016\/j.automatica.2013.05.025","volume":"49","author":"J Ding","year":"2013","unstructured":"Ding, J., Kamgarpour, M., Summers, S., Abate, A., Lygeros, J., Tomlin, C.J.: A stochastic games framework for verification and control of discrete-time stochastic hybrid systems. Automatica 49(9), 2665\u20132674 (2013)","journal-title":"Automatica"},{"issue":"2","key":"1_CR9","doi-asserted-by":"crossref","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":"1_CR10","doi-asserted-by":"crossref","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Aggregation of thermostatically controlled loads by formal abstractions. In: European Control Conference, Zurich, Switzerland, pp. 4232\u20134237, July 2013","DOI":"10.23919\/ECC.2013.6669547"},{"key":"1_CR11","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. LNCS, vol. 8413, pp. 547\u2013561. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_45"},{"issue":"2","key":"1_CR12","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1109\/TAC.2013.2273300","volume":"59","author":"S Esmaeil Zadeh Soudjani","year":"2014","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Probabilistic reach-avoid computation for partially-degenerate stochastic processes. IEEE Trans. Autom. Control 59(2), 528\u2013534 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"SEZ Soudjani","year":"2015","unstructured":"Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST $$^{2}$$ : formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272\u2013286. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_23"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Haesaert, S., Abate, A., Van Den Hof, P.M.J.: Data-driven and model-based verification: a Bayesian identification approach. In: Proceedings of the IEEE Conference on Decision and Control, pp. 6830\u20136835 (2016)","DOI":"10.1109\/CDC.2015.7403295"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-43425-4_16","volume-title":"Quantitative Evaluation of Systems","author":"S Haesaert","year":"2016","unstructured":"Haesaert, S., Abate, A., Hof, P.M.J.: Verification of general Markov decision processes by approximate similarity relations and policy refinement. In: Agha, G., Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 227\u2013243. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-43425-4_16"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Kamgarpour, M., Ellen, C., Esmaeil Zadeh Soudjani, S., Gerwinn, S., Mathieu, J.L., Mullner, N., Abate, A., Callaway, D.S., Fr\u00e4nzle, M., Lygeros, J.: Modeling options for demand side participation of thermostatically controlled loads. In: International Conference on Bulk Power System Dynamics and Control (IREP), pp. 1\u201315, August 2013","DOI":"10.1109\/IREP.2013.6629396"},{"issue":"3","key":"1_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-11(3:8)2015","volume":"11","author":"S Esmaeil Zadeh Soudjani","year":"2015","unstructured":"Esmaeil Zadeh Soudjani, S., 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":"1_CR18","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 515, 1\u201318 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.-P., Abate, A.: Quantitative model checking of controlled discrete-time Markov processes. Inform. Comput. (2016). doi: 10.1016\/j.ic.2016.11.006","DOI":"10.1016\/j.ic.2016.11.006"},{"key":"1_CR20","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1016\/j.sysconle.2014.04.003","volume":"69","author":"M Zamani","year":"2014","unstructured":"Zamani, M., Abate, A.: Symbolic models for randomly switched stochastic systems. Syst. Control Lett. 69, 38\u201346 (2014)","journal-title":"Syst. Control Lett."},{"issue":"5","key":"1_CR21","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/j.automatica.2015.03.004","volume":"55","author":"M Zamani","year":"2015","unstructured":"Zamani, M., Abate, A., Girard, A.: Symbolic models for stochastic switched systems: a discretization and a discretization-free approach. Automatica 55(5), 183\u2013196 (2015)","journal-title":"Automatica"},{"issue":"12","key":"1_CR22","doi-asserted-by":"crossref","first-page":"2825","DOI":"10.1109\/TAC.2014.2351652","volume":"59","author":"M Zamani","year":"2014","unstructured":"Zamani, M., Mohajerin Esfahani, P., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Autom. Control 59(12), 2825\u20132830 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Zamani, M., Mazo, M., Abate, A.: Finite abstractions of networked control systems. In: Proceedings of the 53rd IEEE Conference on Decision and Control, pp. 95\u2013100 (2014)","DOI":"10.1109\/CDC.2014.7039365"}],"container-title":["Lecture Notes in Computer Science","Numerical Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-54292-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T15:03:14Z","timestamp":1568818994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-54292-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319542911","9783319542928"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-54292-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}