{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:29:00Z","timestamp":1742992140832,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031158384"},{"type":"electronic","value":"9783031158391"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15839-1_5","type":"book-chapter","created":{"date-parts":[[2022,8,28]],"date-time":"2022-08-28T18:02:38Z","timestamp":1661709758000},"page":"80-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Robustly Complete Finite-State Abstractions for\u00a0Verification of\u00a0Stochastic Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2923-7154","authenticated-orcid":false,"given":"Yiming","family":"Meng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-2299","authenticated-orcid":false,"given":"Jun","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,29]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78929-1_1","volume-title":"Hybrid Systems: Computation and Control","author":"A Abate","year":"2008","unstructured":"Abate, A., D\u2019Innocenzo, A., Di Benedetto, M.D., Sastry, S.S.: Markov set-chains as abstractions of stochastic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 1\u201315. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_1"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., Katoen, J.P., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 83\u201392 (2011)","DOI":"10.1145\/1967701.1967715"},{"issue":"11","key":"5_CR3","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"},{"key":"5_CR4","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":"5_CR5","series-title":"Studies in Systems, Decision and Control","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7","volume-title":"Formal Methods for Discrete-Time Dynamical Systems","author":"C Belta","year":"2017","unstructured":"Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems. SSDC, vol. 89. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-50763-7"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-27813-9_15","volume-title":"Computer Aided Verification","author":"D Bustan","year":"2004","unstructured":"Bustan, D., Rubin, S., Vardi, M.Y.: Verifying $$\\omega $$-regular properties of Markov chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 189\u2013201. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_15"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Cauchi, N., Laurenti, L., Lahijanian, M., Abate, A., Kwiatkowska, M., Cardelli, L.: Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems. In: Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 240\u2013251 (2019)","DOI":"10.1145\/3302504.3311805"},{"key":"5_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107295513","volume-title":"Stochastic Equations in Infinite Dimensions","author":"G Da Prato","year":"2014","unstructured":"Da Prato, G., Zabczyk, J.: Stochastic Equations in Infinite Dimensions. Cambridge University Press, Cambridge (2014)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Delimpaltadakis, G., Laurenti, L., Mazo Jr., M.: Abstracting the sampling behaviour of stochastic linear periodic event-triggered control systems. arXiv preprint arXiv:2103.13839 (2021)","DOI":"10.1109\/CDC45484.2021.9683751"},{"issue":"7","key":"5_CR11","doi-asserted-by":"publisher","first-page":"2975","DOI":"10.1109\/TAC.2020.3014142","volume":"66","author":"M Dutreix","year":"2020","unstructured":"Dutreix, M., Coogan, S.: Specification-guided verification and abstraction refinement of mixed monotone stochastic systems. IEEE Trans. Autom. Control 66(7), 2975\u20132990 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR12","unstructured":"Dutreix, M.D.H.: Verification and synthesis for stochastic systems with temporal logic specifications. Ph.D. thesis, Georgia Institute of Technology (2020)"},{"issue":"3","key":"5_CR13","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1111\/j.1751-5823.2002.tb00178.x","volume":"70","author":"AL Gibbs","year":"2002","unstructured":"Gibbs, A.L., Su, F.E.: On choosing and bounding probability metrics. Int. Stat. Rev. 70(3), 419\u2013435 (2002)","journal-title":"Int. Stat. Rev."},{"issue":"1","key":"5_CR14","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TAC.2009.2034922","volume":"55","author":"A Girard","year":"2009","unstructured":"Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116\u2013126 (2009)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1\u20132","key":"5_CR15","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S., Dean, T.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"5_CR16","volume-title":"Markov Set-Chains","author":"DJ Hartfiel","year":"2006","unstructured":"Hartfiel, D.J.: Markov Set-Chains. Springer, Heidelberg (2006)"},{"issue":"1","key":"5_CR17","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1109\/TAC.2007.914952","volume":"53","author":"M Kloetzer","year":"2008","unstructured":"Kloetzer, M., Belta, C.: A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Autom. Control 53(1), 287\u2013297 (2008)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"8","key":"5_CR18","doi-asserted-by":"publisher","first-page":"2031","DOI":"10.1109\/TAC.2015.2398883","volume":"60","author":"M Lahijanian","year":"2015","unstructured":"Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60(8), 2031\u20132045 (2015)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3","key":"5_CR19","doi-asserted-by":"publisher","first-page":"1199","DOI":"10.1109\/TAC.2020.2987711","volume":"66","author":"Y Li","year":"2020","unstructured":"Li, Y., Liu, J.: Robustly complete synthesis of memoryless controllers for nonlinear systems with reach-and-stay specifications. IEEE Trans. Autom. Control 66(3), 1199\u20131206 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Liu, J.: Robust abstractions for control synthesis: completeness via robustness for linear-time properties. In: Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 101\u2013110 (2017)","DOI":"10.1145\/3049797.3049826"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-030-85037-1_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Liu","year":"2021","unstructured":"Liu, J.: Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability. In: Dima, C., Shirmohammadi, M. (eds.) FORMATS 2021. LNCS, vol. 12860, pp. 67\u201383. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85037-1_5"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Mallik, K., Soudjani, S.: Symbolic controller synthesis for b\u00fcchi specifications on stochastic systems. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2020)","DOI":"10.1145\/3365365.3382214"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Meng, Y., Liu, J.: Robustly complete finite-state abstractions for verification of stochastic systems. arXiv preprint arXiv:2205.01854 (2022)","DOI":"10.1007\/978-3-031-15839-1_5"},{"key":"5_CR24","unstructured":"Parker, D.: Verification of probabilistic real-time systems. In: Proceedings of 2013 Real-Time Systems Summer School (ETR 2013) (2013)"},{"issue":"10","key":"5_CR25","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1016\/j.automatica.2008.02.021","volume":"44","author":"G Pola","year":"2008","unstructured":"Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508\u20132516 (2008)","journal-title":"Automatica"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Ramponi, F., Chatterjee, D., Summers, S., Lygeros, J.: On the connections between PCTL and dynamic programming. In: Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 253\u2013262 (2010)","DOI":"10.1145\/1755952.1755988"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Rogers, L.C.G., Williams, D.: Diffusions, Markov Processes and Martingales, Volume 1: Foundations. Cambridge Mathematical Library (2000)","DOI":"10.1017\/CBO9781107590120"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Soudjani, S.E.Z., Abate, A.: Adaptive gridding for abstraction and verification of stochastic hybrid systems. In: 2011 Eighth International Conference on Quantitative Evaluation of SysTems, pp. 59\u201368. IEEE (2011)","DOI":"10.1109\/QEST.2011.16"},{"issue":"12","key":"5_CR29","doi-asserted-by":"publisher","first-page":"1951","DOI":"10.1016\/j.automatica.2010.08.006","volume":"46","author":"S Summers","year":"2010","unstructured":"Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem. Automatica 46(12), 1951\u20131961 (2010)","journal-title":"Automatica"},{"issue":"12","key":"5_CR30","doi-asserted-by":"publisher","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada, P., Pappas, G.J.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862\u20131877 (2006)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: On infinite-horizon probabilistic properties and stochastic bisimulation functions. In: 2011 50th IEEE Conference on Decision and Control and European Control Conference, pp. 526\u2013531. IEEE (2011)","DOI":"10.1109\/CDC.2011.6160617"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Regularization of bellman equations for infinite-horizon probabilistic properties. In: Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 227\u2013236 (2012)","DOI":"10.1145\/2185632.2185666"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 283\u2013292 (2013)","DOI":"10.1145\/2461328.2461372"},{"key":"5_CR34","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. Theoret. Comput. Sci. 515, 1\u201318 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2016.11.006","volume":"253","author":"I Tkachev","year":"2017","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.P., Abate, A.: Quantitative model-checking of controlled discrete-time Markov processes. Inf. Comput. 253, 1\u201335 (2017)","journal-title":"Inf. Comput."},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite state programs. In: 26th Annual Symposium on Foundations of Computer Science (FOCS), pp. 327\u2013338. IEEE (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"5","key":"5_CR37","doi-asserted-by":"publisher","first-page":"471","DOI":"10.3390\/math9050471","volume":"9","author":"PC Vassiliou","year":"2021","unstructured":"Vassiliou, P.C.: Non-homogeneous Markov set systems. Mathematics 9(5), 471 (2021)","journal-title":"Mathematics"},{"issue":"8\u20139","key":"5_CR38","doi-asserted-by":"publisher","first-page":"945","DOI":"10.1016\/j.artint.2007.12.002","volume":"172","author":"D Wu","year":"2008","unstructured":"Wu, D., Koutsoukos, X.: Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. Artif. Intell. 172(8\u20139), 945\u2013954 (2008)","journal-title":"Artif. Intell."}],"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-031-15839-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T23:15:23Z","timestamp":1662074123000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15839-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031158384","9783031158391"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15839-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"formats2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}