{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:23:46Z","timestamp":1776889426165,"version":"3.51.2"},"reference-count":34,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["European Journal of Control"],"published-print":{"date-parts":[[2012,1]]},"DOI":"10.3166\/ejc.18.572-587","type":"journal-article","created":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T18:33:22Z","timestamp":1374777202000},"page":"572-587","source":"Crossref","is-referenced-by-count":24,"title":["Safety Verification for Probabilistic Hybrid Systems"],"prefix":"10.1016","volume":"18","author":[{"given":"Lijun","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Zhikun","family":"She","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Ratschan","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"11","key":"10.3166\/EJC.18.572-587_bib0005","doi-asserted-by":"crossref","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","article-title":"Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems","volume":"44","author":"Abate","year":"2008","journal-title":"Automatica"},{"issue":"6","key":"10.3166\/EJC.18.572-587_bib0010","doi-asserted-by":"crossref","first-page":"2070","DOI":"10.1137\/S0363012995279985","article-title":"Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process","volume":"35","author":"Altman","year":"1997","journal-title":"SIAM J Control Optim"},{"issue":"1","key":"10.3166\/EJC.18.572-587_bib0015","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur","year":"1995","journal-title":"Theor Comput Sci"},{"issue":"1","key":"10.3166\/EJC.18.572-587_bib0020","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1145\/1132357.1132363","article-title":"Predicate abstraction for reachability analysis of hybrid systems","volume":"5","author":"Alur","year":"2006","journal-title":"ACM Trans Embedded Comput Syst"},{"key":"10.3166\/EJC.18.572-587_bib0025","series-title":"Stochastic Differential Equations: Theory and Applications","author":"Arnold","year":"1974"},{"key":"10.3166\/EJC.18.572-587_bib0030","volume":"Vol. 2","author":"Bertsekas","year":"1995"},{"key":"10.3166\/EJC.18.572-587_bib0035","first-page":"499","article-title":"Model checking of probabilistic and nondeterministic systems","volume":"Vol. 1026","author":"Bianco","year":"1995"},{"key":"10.3166\/EJC.18.572-587_bib0040","volume":"Vol. 337","author":"Blom","year":"2006"},{"key":"10.3166\/EJC.18.572-587_bib0045","first-page":"234","article-title":"Extended stochastic hybrid systems and their reachability problem","volume":"Vol. 2993","author":"Bujorianu","year":"2004"},{"key":"10.3166\/EJC.18.572-587_bib0050","doi-asserted-by":"crossref","unstructured":"Bujorianu ML, Lygeros J. Toward a general theory of stochastic hybrid systems. In Blom and Lygeros [8], 3\u201330.","DOI":"10.1007\/11587392_1"},{"key":"10.3166\/EJC.18.572-587_bib0055","first-page":"198","article-title":"Bisimulation for general stochastic hybrid systems","volume":"Vol. 3414","author":"Bujorianu","year":"2005"},{"key":"10.3166\/EJC.18.572-587_bib0060","first-page":"610","article-title":"Reachability analysis of stochastic hybrid systems by optimal control","volume":"Vol. 4981","author":"Bujorianu","year":"2008"},{"key":"10.3166\/EJC.18.572-587_bib0065","first-page":"192","article-title":"Verification of hybrid systems based on counterexampleguided abstraction refinement","volume":"Vol. 2619","author":"Clarke","year":"2003"},{"key":"10.3166\/EJC.18.572-587_bib0070","first-page":"39","article-title":"Reachability analysis of probabilistic systems by successive refinements","volume":"Vol. 2165","author":"D\u2019Argenio","year":"2001"},{"issue":"3","key":"10.3166\/EJC.18.572-587_bib0075","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1111\/j.2517-6161.1984.tb01308.x","article-title":"Piecewise-deterministic Markov processes: A general class of non-diffusion stochastic models","volume":"46","author":"Davis","year":"1984","journal-title":"J R Stat Soc"},{"key":"10.3166\/EJC.18.572-587_bib0080","first-page":"172","article-title":"Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems","volume":"Vol. 4981","author":"Fr\u00e4nzle","year":"2008"},{"key":"10.3166\/EJC.18.572-587_bib0085","first-page":"258","article-title":"Algorithmic verification of hybrid systems past HyTech","volume":"Vol. 3414","author":"Frehse","year":"2005"},{"key":"10.3166\/EJC.18.572-587_bib0090","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","article-title":"What's decidable about hybrid automata","volume":"57","author":"Henzinger","year":"1998","journal-title":"J Comput Syst Sci"},{"key":"10.3166\/EJC.18.572-587_bib0095","first-page":"162","article-title":"Probabilistic CEGAR","volume":"Vol. 5123","author":"Hermanns","year":"2008"},{"key":"10.3166\/EJC.18.572-587_bib0100","first-page":"160","article-title":"Towards a theory of stochastic hybrid systems","volume":"Vol. 1790","author":"Hu","year":"2005"},{"key":"10.3166\/EJC.18.572-587_bib0105","first-page":"266","article-title":"Specification and refinement of probabilistic processes. IEEE Symposium on Logic in Computer Science (LICS)","author":"Jonsson","year":"1991","journal-title":"IEEE Computer Society"},{"key":"10.3166\/EJC.18.572-587_bib0110","first-page":"318","article-title":"Approximate abstraction of stochastic hybrid automata","volume":"Vol. 3927","author":"Julius","year":"2006"},{"issue":"6","key":"10.3166\/EJC.18.572-587_bib0115","doi-asserted-by":"crossref","first-page":"1193","DOI":"10.1109\/TAC.2009.2019791","article-title":"Approximations of stochastic hybrid systems","volume":"54","author":"Julius","year":"2009","journal-title":"IEEE Trans Autom Control"},{"key":"10.3166\/EJC.18.572-587_bib0120","first-page":"212","article-title":"Stochastic Games for verification of probabilistic timed automata","volume":"Vol. 5813","author":"Kwiatkowska","year":"2009"},{"issue":"1","key":"10.3166\/EJC.18.572-587_bib0125","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","article-title":"Automatic verification of real-time systems with discrete probability distributions","volume":"282","author":"Kwiatkowska","year":"2002","journal-title":"Theor Comput Sci"},{"key":"10.3166\/EJC.18.572-587_bib0130","first-page":"137","article-title":"A new class of decidable hybrid systems","volume":"Vol. 1569","author":"Lafferriere","year":"1999"},{"key":"10.3166\/EJC.18.572-587_bib0135","first-page":"228","article-title":"An algorithm for the approximative analysis of rectangular automata","volume":"Vol. 1486","author":"Preu\u00dfig","year":"1998"},{"key":"10.3166\/EJC.18.572-587_bib0140","series-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman","year":"1994"},{"key":"10.3166\/EJC.18.572-587_bib0145","series-title":"TAMC 2010: 7th Annual Conference on Theory and Applications of Models of Computation, LNCS","first-page":"397","article-title":"Safety verification of non-linear hybrid systems is quasi-semidecidable","author":"Ratschan","year":"2010"},{"issue":"1","key":"10.3166\/EJC.18.572-587_bib0150","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1210268.1210276","article-title":"Safety verification of hybrid systems by constraint propagation-based abstraction refinement","volume":"6","author":"Ratschan","year":"2007","journal-title":"ACM Trans Embedded Comput Syst"},{"issue":"2","key":"10.3166\/EJC.18.572-587_bib0155","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala","year":"1995","journal-title":"J Comput (NJC)"},{"key":"10.3166\/EJC.18.572-587_bib0160","first-page":"31","article-title":"Decidable model checking of probabilistic hybrid automata","volume":"Vol. 1926","author":"Sproston","year":"2000"},{"key":"10.3166\/EJC.18.572-587_bib0165","series-title":"Analysis and Design of Hybrid Systems (ADHS)","first-page":"162","article-title":"Constraint-based analysis of probabilistic hybrid systems","author":"Teige","year":"2009"},{"key":"10.3166\/EJC.18.572-587_bib0170","first-page":"196","article-title":"Safety verification for probabilistic hybrid systems","volume":"Vol. 6174","author":"Zhang","year":"2010"}],"container-title":["European Journal of Control"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0947358012711597?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0947358012711597?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,5,15]],"date-time":"2024-05-15T10:50:06Z","timestamp":1715770206000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0947358012711597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":34,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["S0947358012711597"],"URL":"https:\/\/doi.org\/10.3166\/ejc.18.572-587","relation":{},"ISSN":["0947-3580"],"issn-type":[{"value":"0947-3580","type":"print"}],"subject":[],"published":{"date-parts":[[2012,1]]}}}