{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T21:32:25Z","timestamp":1772314345471,"version":"3.50.1"},"reference-count":23,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100018703","name":"European Innovation Council (EIC) Project","doi-asserted-by":"publisher","award":["SymAware 101070802"],"award-info":[{"award-number":["SymAware 101070802"]}],"id":[{"id":"10.13039\/100018703","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council (ERC) Project","doi-asserted-by":"publisher","award":["Auto-CyPheR 101089047"],"award-info":[{"award-number":["Auto-CyPheR 101089047"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DFG Project","award":["389792660 (TRR 248\u2013CPEC)"],"award-info":[{"award-number":["389792660 (TRR 248\u2013CPEC)"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Control Syst. Lett."],"published-print":{"date-parts":[[2024]]},"DOI":"10.1109\/lcsys.2024.3507279","type":"journal-article","created":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T19:50:23Z","timestamp":1732737023000},"page":"2703-2708","source":"Crossref","is-referenced-by-count":4,"title":["Necessary and Sufficient Certificates for Almost Sure Reachability"],"prefix":"10.1109","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8544-9426","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5187-5415","authenticated-orcid":false,"given":"V. R.","family":"Sathiyanarayana","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-6678","authenticated-orcid":false,"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_18"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2011.6161499"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2019.8796030"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE55969.2022.00034"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.3013916"},{"key":"ref7","volume-title":"Foundations of Modern Probability (Probability and its Applications)","author":"Kallenberg","year":"2002"},{"key":"ref8","volume-title":"Nonlinear Systems","author":"Khalil","year":"2001"},{"key":"ref9","volume-title":"Stochastic Stability and Control","author":"Kushner","year":"1967"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2019.2917975"},{"key":"ref12","first-page":"1","article-title":"Sound and complete proof rules for probabilistic termination","volume-title":"Proc. ACM Program. Lang.","author":"Majumdar"},{"key":"ref13","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver","year":"2005"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3267-7"},{"key":"ref16","volume-title":"SOSTOOLS: Sum of squares optimization toolbox for MATLAB","author":"Papachristodoulou","year":"2021"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.3182\/20050703-6-CZ-1902.00743"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2020.109439"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511662478"},{"key":"ref21","volume-title":"General Topology","author":"Willard","year":"2012"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2476155"},{"key":"ref23","article-title":"Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems","author":"Xue","year":"2024","journal-title":"arXiv:2408.15572"}],"container-title":["IEEE Control Systems Letters"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/7782633\/10411713\/10769425.pdf?arnumber=10769425","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,16]],"date-time":"2024-12-16T19:35:00Z","timestamp":1734377700000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10769425\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/lcsys.2024.3507279","relation":{},"ISSN":["2475-1456"],"issn-type":[{"value":"2475-1456","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]}}}