{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T11:53:28Z","timestamp":1787313208372,"version":"build-2736575974"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100007219","name":"Shanghai Natural Science Foundation","doi-asserted-by":"crossref","award":["17ZR1408300"],"award-info":[{"award-number":["17ZR1408300"]}],"id":[{"id":"10.13039\/100007219","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61632015, 61561146394, 61602348 and 11471209"],"award-info":[{"award-number":["61632015, 61561146394, 61602348 and 11471209"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004543","name":"China Scholarship Council","doi-asserted-by":"crossref","award":["201606190185"],"award-info":[{"award-number":["201606190185"]}],"id":[{"id":"10.13039\/501100004543","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>The problem of probabilistic safety verification of stochastic hybrid systems is to check whether the probability that a given system will reach an unsafe region from certain initial states can be bounded by some given probability threshold. The paper considers stochastic hybrid systems where the behavior is governed by polynomial equalities and inequalities, as for usual hybrid systems, but the initial states follow some stochastic distributions. It proposes a new barrier certificate based method for probabilistic safety verification which guarantees the absolute safety in a infinite time horizon that is beyond the reach of existing techniques using either statistical model checking or probabilistic reachable set computation. It also gives a novel computational approach, by building and solving a constrained optimization problem coming from verification conditions of barrier certificates, to compute the lower bound on safety probabilities which can be compared with the given threshold. Experimental evidence is provided demonstrating the applicability of our approach on several benchmarks.<\/jats:p>","DOI":"10.1145\/3126508","type":"journal-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T08:33:53Z","timestamp":1506501233000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":56,"title":["Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates"],"prefix":"10.1145","volume":"16","author":[{"given":"Chao","family":"Huang","sequence":"first","affiliation":[{"name":"State Key Lab for Novel Software Technology, Nanjing University, Jiangsu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"State Key Lab for Novel Software Technology, Nanjing University, Jiangsu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wang","family":"Lin","sequence":"additional","affiliation":[{"name":"Key Lab of Mathematics Mechanization, AMSS, CAS, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhengfeng","family":"Yang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"State Key Lab for Novel Software Technology, Nanjing University, Jiangsu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2008.4621131"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039472"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_16"},{"key":"e_1_2_1_7_1","volume-title":"Bujorianu and John Lygeros","author":"Manuela","year":"2003"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2016.07.010"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","volume-title":"Discretizing Affine Hybrid Automata with Uncertainty","author":"Dang Thao","DOI":"10.1007\/978-3-642-24372-1_36"},{"key":"e_1_2_1_10_1","first-page":"128","article-title":"Reachability Analysis for Polynomial Dynamical Systems Using the Bernstein Expansion","volume":"17","author":"Dang Thao","year":"2012","journal-title":"Reliable Computing"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0329-y"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967710"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_25"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0167-z"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_26"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2014.09.001"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/646880.710449"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_25"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562139"},{"key":"e_1_2_1_20_1","volume-title":"Computer Aided Verification","author":"Kong Hui"},{"key":"e_1_2_1_21_1","unstructured":"Michal Ko\u010dvara and Michael Stingl. 2005. PENBMI User\u2019s guide (Version 2.0). (2005). Available at http:\/\/www.penopt.com.  Michal Ko\u010dvara and Michael Stingl. 2005. PENBMI User\u2019s guide (Version 2.0). (2005). Available at http:\/\/www.penopt.com."},{"key":"e_1_2_1_22_1","volume-title":"Symbolic model checking for probabilistic timed automata. Lecture notes in computer science 3253","author":"Kwiatkowska Marta","year":"2004"},{"key":"e_1_2_1_23_1","volume-title":"Larsen and Axel Legay","author":"Kim","year":"2016"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0384-z"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032300"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"e_1_2_1_27_1","volume-title":"Decision and Control, 2004. CDC. 43rd IEEE Conference on","volume":"1","author":"Prajna Stephen"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1210268.1210276"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.3182\/20130904-3-FR-2041.00198"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_12"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728625"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_10"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_13"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646846.706977"},{"key":"e_1_2_1_36_1","volume-title":"Clarke","author":"Wang Qinsi","year":"2015"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968478.2968484"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_21"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126508","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126508","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:01Z","timestamp":1750259101000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126508"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,27]]},"references-count":37,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3126508"],"URL":"https:\/\/doi.org\/10.1145\/3126508","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,27]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}