{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:05Z","timestamp":1750220405417,"version":"3.41.0"},"reference-count":82,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2021,11,15]],"date-time":"2021-11-15T00:00:00Z","timestamp":1636934400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2021,11,30]]},"abstract":"<jats:p>We present a scalable methodology to verify stochastic hybrid systems for inequality linear temporal logic (iLTL) or inequality metric interval temporal logic (iMITL). Using the Mori\u2013Zwanzig reduction method, we construct a finite-state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. Based on this, we propose the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in iLTL or iMITL. The scalability of the proposed algorithms is demonstrated by a case study.<\/jats:p>","DOI":"10.1145\/3483380","type":"journal-article","created":{"date-parts":[[2021,11,15]],"date-time":"2021-11-15T17:20:42Z","timestamp":1636996842000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction"],"prefix":"10.1145","volume":"20","author":[{"given":"Yu","family":"Wang","sequence":"first","affiliation":[{"name":"University of Florida, Gainesville, FL"}]},{"given":"Nima","family":"Roohi","sequence":"additional","affiliation":[{"name":"Amazon, Seattle, WA"}]},{"given":"Matthew","family":"West","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL"}]},{"given":"Geir E.","family":"Dullerud","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL"}]}],"member":"320","published-online":{"date-parts":[[2021,11,15]]},"reference":[{"unstructured":"Commons Math: The Apache Commons Mathematics Library. Retrieved June 10 2019 from https:\/\/commons.apache.org\/proper\/commons-math.","key":"e_1_3_2_2_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_3_2","DOI":"10.1109\/TAC.2011.2160595"},{"doi-asserted-by":"publisher","key":"e_1_3_2_4_2","DOI":"10.3166\/ejc.16.624-641"},{"doi-asserted-by":"publisher","key":"e_1_3_2_5_2","DOI":"10.1007\/978-3-319-06880-0_2"},{"issue":"3","key":"e_1_3_2_6_2","first-page":"1","article-title":"Quantitative approximation of the probability distribution of a Markov process by formal abstractions","volume":"11","author":"Abate Alessandro","year":"2015","unstructured":"Alessandro Abate and Sadegh E. Z. Soudjani. 2015. Quantitative approximation of the probability distribution of a Markov process by formal abstractions. Logical Methods in Computer Science 11, 3 (2015), 1\u201329.","journal-title":"Logical Methods in Computer Science"},{"doi-asserted-by":"publisher","key":"e_1_3_2_7_2","DOI":"10.1145\/2432622.2432626"},{"doi-asserted-by":"publisher","key":"e_1_3_2_8_2","DOI":"10.5555\/1765871.1765891"},{"doi-asserted-by":"publisher","key":"e_1_3_2_9_2","DOI":"10.1016\/0304-3975(94)90010-8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_10_2","DOI":"10.1145\/227595.227602"},{"doi-asserted-by":"publisher","key":"e_1_3_2_11_2","DOI":"10.5555\/647769.733948"},{"doi-asserted-by":"publisher","key":"e_1_3_2_12_2","DOI":"10.1145\/2432622.2432626"},{"doi-asserted-by":"publisher","key":"e_1_3_2_13_2","DOI":"10.1109\/CDC.2009.5400343"},{"doi-asserted-by":"publisher","key":"e_1_3_2_14_2","DOI":"10.1201\/9781315221625"},{"doi-asserted-by":"publisher","key":"e_1_3_2_15_2","DOI":"10.1145\/1838552.1838553"},{"doi-asserted-by":"publisher","key":"e_1_3_2_16_2","DOI":"10.1073\/pnas.97.7.2968"},{"doi-asserted-by":"publisher","key":"e_1_3_2_17_2","DOI":"10.1214\/aoms\/1177700156"},{"doi-asserted-by":"publisher","key":"e_1_3_2_18_2","DOI":"10.1142\/S012905410300190X"},{"doi-asserted-by":"publisher","key":"e_1_3_2_19_2","DOI":"10.5555\/3264692"},{"doi-asserted-by":"publisher","key":"e_1_3_2_20_2","DOI":"10.1007\/978-3-319-10575-8_13"},{"key":"e_1_3_2_21_2","article-title":"Statistical model checking for stochastic hybrid systems","author":"David Alexandre","year":"2012","unstructured":"Alexandre David, Dehui Du, Kim G. Larsen, Axel Legay, Marius Miku\u010dionis, Danny B\u00f8gsted Poulsen, and Sean Sedwards. 2012. Statistical model checking for stochastic hybrid systems. arXiv:1208.3856. Retrieved from https:\/\/arxiv.org\/abs\/1208.3856.","journal-title":"arXiv:1208.3856"},{"doi-asserted-by":"publisher","key":"e_1_3_2_22_2","DOI":"10.1137\/S0036142996313002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_23_2","DOI":"10.1006\/inco.2001.2962"},{"key":"e_1_3_2_24_2","volume-title":"A Course in Robust Control Theory: A Convex Approach","author":"Dullerud Geir E.","year":"2013","unstructured":"Geir E. Dullerud and Fernando Paganini. 2013. A Course in Robust Control Theory: A Convex Approach. Springer Science & Business Media."},{"doi-asserted-by":"publisher","key":"e_1_3_2_25_2","DOI":"10.5555\/2227508.2227516"},{"doi-asserted-by":"publisher","key":"e_1_3_2_26_2","DOI":"10.5555\/1032659.1034190"},{"doi-asserted-by":"publisher","key":"e_1_3_2_27_2","DOI":"10.1137\/120871456"},{"doi-asserted-by":"publisher","key":"e_1_3_2_28_2","DOI":"10.1145\/1967701.1967710"},{"doi-asserted-by":"publisher","key":"e_1_3_2_29_2","DOI":"10.5555\/647770.734262"},{"doi-asserted-by":"publisher","key":"e_1_3_2_30_2","DOI":"10.1109\/TAC.2009.2034922"},{"doi-asserted-by":"publisher","key":"e_1_3_2_31_2","DOI":"10.1007\/978-3-319-26916-0_6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_32_2","DOI":"10.1137\/16M1079397"},{"doi-asserted-by":"publisher","key":"e_1_3_2_33_2","DOI":"10.5555\/1349745"},{"doi-asserted-by":"publisher","key":"e_1_3_2_34_2","DOI":"10.1007\/BF01211866"},{"doi-asserted-by":"publisher","key":"e_1_3_2_35_2","DOI":"10.1002\/rnc.1017"},{"doi-asserted-by":"publisher","key":"e_1_3_2_36_2","DOI":"10.5555\/646880.710449"},{"doi-asserted-by":"publisher","key":"e_1_3_2_37_2","DOI":"10.1007\/978-3-540-24743-2_28"},{"doi-asserted-by":"publisher","key":"e_1_3_2_38_2","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"e_1_3_2_39_2","volume-title":"Proceedings of the 1st International Workshop on Applied Verification for Continuous and Hybrid Systems","author":"Jin Xiaoqing","year":"2014","unstructured":"Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. 2014. Benchmarks for model transformations and conformance checking. In Proceedings of the 1st International Workshop on Applied Verification for Continuous and Hybrid Systems."},{"doi-asserted-by":"publisher","key":"e_1_3_2_40_2","DOI":"10.1109\/TAC.2009.2019791"},{"key":"e_1_3_2_41_2","volume-title":"Brownian Motion and Stochastic Calculus","author":"Karatzas Ioannis","year":"2012","unstructured":"Ioannis Karatzas and Steven Shreve. 2012. Brownian Motion and Stochastic Calculus. Vol. 113. Springer Science & Business Media."},{"doi-asserted-by":"publisher","key":"e_1_3_2_42_2","DOI":"10.1109\/TAC.2007.914952"},{"doi-asserted-by":"publisher","key":"e_1_3_2_43_2","DOI":"10.1109\/TSMCA.2007.914777"},{"doi-asserted-by":"publisher","key":"e_1_3_2_44_2","DOI":"10.1007\/978-3-540-30482-1_21"},{"doi-asserted-by":"publisher","key":"e_1_3_2_45_2","DOI":"10.1109\/TSE.2010.80"},{"doi-asserted-by":"crossref","unstructured":"Abolfazl Lavaei Sadegh Soudjani Alessandro Abate and Majid Zamani. 2021. Automated verification and synthesis of stochastic hybrid systems: A survey. https:\/\/arxiv.org\/abs\/2101.07491. Preprint.","key":"e_1_3_2_46_2","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"e_1_3_2_47_2","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"Lee Edward Ashford","year":"2017","unstructured":"Edward Ashford Lee and Sanjit A. Seshia. 2017. Introduction to Embedded Systems: A Cyber-Physical Systems Approach. Mit Press."},{"doi-asserted-by":"publisher","key":"e_1_3_2_48_2","DOI":"10.5555\/1939399.1939412"},{"doi-asserted-by":"publisher","key":"e_1_3_2_49_2","DOI":"10.1007\/s10009-015-0384-z"},{"doi-asserted-by":"publisher","key":"e_1_3_2_50_2","DOI":"10.1093\/bioinformatics\/bts166"},{"doi-asserted-by":"publisher","key":"e_1_3_2_51_2","DOI":"10.1016\/j.tcs.2011.01.021"},{"doi-asserted-by":"publisher","key":"e_1_3_2_52_2","DOI":"10.1109\/TAC.2013.2246095"},{"doi-asserted-by":"publisher","key":"e_1_3_2_53_2","DOI":"10.1109\/SFCS.1977.32"},{"doi-asserted-by":"publisher","key":"e_1_3_2_54_2","DOI":"10.1016\/j.automatica.2008.02.021"},{"key":"e_1_3_2_55_2","volume-title":"Continuous Martingales and Brownian Motion","author":"Revuz Daniel","year":"2013","unstructured":"Daniel Revuz and Marc Yor. 2013. Continuous Martingales and Brownian Motion. Vol. 293. Springer Science & Business Media."},{"key":"e_1_3_2_56_2","volume-title":"Monte Carlo Statistical Methods","author":"Robert Christian","year":"2013","unstructured":"Christian Robert and George Casella. 2013. Monte Carlo Statistical Methods. Springer Science & Business Media."},{"doi-asserted-by":"publisher","key":"e_1_3_2_57_2","DOI":"10.1007\/978-3-662-54577-5_33"},{"doi-asserted-by":"publisher","key":"e_1_3_2_58_2","DOI":"10.1007\/978-3-319-73721-8_22"},{"doi-asserted-by":"publisher","key":"e_1_3_2_59_2","DOI":"10.1145\/3049797.3049804"},{"doi-asserted-by":"publisher","key":"e_1_3_2_60_2","DOI":"10.1007\/11513988_26"},{"doi-asserted-by":"publisher","key":"e_1_3_2_61_2","DOI":"10.1098\/rsta.2010.0211"},{"doi-asserted-by":"publisher","key":"e_1_3_2_62_2","DOI":"10.1145\/3503823.3503837"},{"doi-asserted-by":"publisher","key":"e_1_3_2_63_2","DOI":"10.1007\/978-3-319-66335-7_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_64_2","DOI":"10.1109\/ISGTEurope.2012.6465655"},{"doi-asserted-by":"publisher","key":"e_1_3_2_65_2","DOI":"10.1016\/j.nahs.2016.08.003"},{"doi-asserted-by":"publisher","key":"e_1_3_2_66_2","DOI":"10.1016\/j.automatica.2010.08.006"},{"doi-asserted-by":"publisher","key":"e_1_3_2_67_2","DOI":"10.1109\/TAC.2006.886494"},{"key":"e_1_3_2_68_2","first-page":"329","volume-title":"Recent Developments in Stability Theory for Stochastic Hybrid Inclusions","author":"Teel Andrew R.","year":"2017","unstructured":"Andrew R. Teel. 2017. Recent Developments in Stability Theory for Stochastic Hybrid Inclusions. Springer International Publishing, Cham, 329\u2013354."},{"doi-asserted-by":"publisher","key":"e_1_3_2_69_2","DOI":"10.1109\/CDC.2015.7402688"},{"doi-asserted-by":"publisher","key":"e_1_3_2_70_2","DOI":"10.1016\/j.automatica.2014.08.006"},{"doi-asserted-by":"publisher","key":"e_1_3_2_71_2","DOI":"10.1145\/2461328.2461372"},{"doi-asserted-by":"publisher","key":"e_1_3_2_72_2","DOI":"10.1145\/2461328.2461373"},{"doi-asserted-by":"publisher","key":"e_1_3_2_73_2","DOI":"10.1214\/aoms\/1177731118"},{"doi-asserted-by":"publisher","key":"e_1_3_2_74_2","DOI":"10.1016\/j.ifacol.2015.11.186"},{"doi-asserted-by":"publisher","key":"e_1_3_2_75_2","DOI":"10.1145\/2728606.2728627"},{"doi-asserted-by":"publisher","key":"e_1_3_2_76_2","DOI":"10.1109\/CDC.2016.7798719"},{"doi-asserted-by":"publisher","key":"e_1_3_2_77_2","DOI":"10.1145\/1755952.1755968"},{"doi-asserted-by":"publisher","key":"e_1_3_2_78_2","DOI":"10.1007\/11609773_10"},{"doi-asserted-by":"publisher","key":"e_1_3_2_79_2","DOI":"10.1016\/j.ic.2006.05.002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_80_2","DOI":"10.1109\/TAC.2014.2351652"},{"doi-asserted-by":"publisher","key":"e_1_3_2_81_2","DOI":"10.1109\/TAC.2011.2176409"},{"doi-asserted-by":"publisher","key":"e_1_3_2_82_2","DOI":"10.1145\/2185632.2185665"},{"doi-asserted-by":"publisher","key":"e_1_3_2_83_2","DOI":"10.1145\/1755952.1755987"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3483380","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3483380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:58Z","timestamp":1750191538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3483380"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,15]]},"references-count":82,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,11,30]]}},"alternative-id":["10.1145\/3483380"],"URL":"https:\/\/doi.org\/10.1145\/3483380","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2021,11,15]]},"assertion":[{"value":"2020-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}