{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T15:03:21Z","timestamp":1782313401646,"version":"3.54.5"},"reference-count":32,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010,1]]},"DOI":"10.3166\/ejc.16.624-641","type":"journal-article","created":{"date-parts":[[2011,2,8]],"date-time":"2011-02-08T16:16:50Z","timestamp":1297181810000},"page":"624-641","source":"Crossref","is-referenced-by-count":145,"title":["Approximate Model Checking of Stochastic Hybrid Systems"],"prefix":"10.1016","volume":"16","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Lygeros","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maria","family":"Prandini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.3166\/ejc.16.624-641_bib0005","series-title":"Hybrid Systems: Computation and Control, number 4416 in Lecture Notes in Computer Sciences","first-page":"4","article-title":"Computational approaches to reachability analysis of stochastic hybrid systems","author":"Abate","year":"2007"},{"issue":"11","key":"10.3166\/ejc.16.624-641_bib0010","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"},{"key":"10.3166\/ejc.16.624-641_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"},{"key":"10.3166\/ejc.16.624-641_bib0020","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor Comput Sci"},{"issue":"7","key":"10.3166\/ejc.16.624-641_bib0025","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","article-title":"Discrete abstractions of hybrid systems","volume":"88","author":"Alur","year":"2000","journal-title":"Proc IEEE"},{"key":"10.3166\/ejc.16.624-641_bib0030","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.3166\/ejc.16.624-641_bib0035","series-title":"Concurrency Theory, number 1664 in Lecture Notes in Computer Sciences","first-page":"146","article-title":"Approximate symbolic model checking of continous-time Markov chains","author":"Baier","year":"1999"},{"issue":"3","key":"10.3166\/ejc.16.624-641_bib0040","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1109\/TAC.1975.1100984","article-title":"Convergence of discretization procedures in dynamic programming","volume":"20","author":"Bertsekas","year":"1975","journal-title":"IEEE Trans Autom Control"},{"key":"10.3166\/ejc.16.624-641_bib0045","article-title":"Stochastic Optimal Control: The Discrete-Time Case","author":"Bertsekas","year":"1996","journal-title":"Athena Scientific"},{"key":"10.3166\/ejc.16.624-641_bib0050","series-title":"Stochastic Hybrid Systems: Theory and Safety Critical Applications. Number 337 in Lecture Notes in Control and Information Sciences","author":"Blom","year":"2006"},{"key":"10.3166\/ejc.16.624-641_bib0055","series-title":"Hybrid Systems: Computation and Control, number 2993 in Lecture Notes in Computer Sciences","first-page":"234","article-title":"Extended stochastic hybrid systems and their reachability problem","author":"Bujorianu","year":"2004"},{"key":"10.3166\/ejc.16.624-641_bib0060","series-title":"Hybrid Systems: Computation and Control, number 2623 in Lecture Notes in Computer Sciences","first-page":"126","article-title":"Reachability questions in piecewise deterministic Markov processes","author":"Bujorianu","year":"2003"},{"key":"10.3166\/ejc.16.624-641_bib0065","series-title":"Stochastic Hybrid Systems. Number 24 in Control Engineering","author":"Cassandras","year":"2006"},{"key":"10.3166\/ejc.16.624-641_bib0070","article-title":"Model Checking","author":"Clarke","year":"1999","journal-title":"MIT Press"},{"issue":"4","key":"10.3166\/ejc.16.624-641_bib0075","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","article-title":"The complexity of probabilistic verification","volume":"42","author":"Courcoubetis","year":"1995","journal-title":"J ACM"},{"key":"10.3166\/ejc.16.624-641_bib0080","series-title":"Markov Models and Optimization","author":"Davis","year":"1993"},{"key":"10.3166\/ejc.16.624-641_bib0085","unstructured":"de Alfaro L. Formal Verification of Probabilistic Systems. PhD thesis, Department of Computer Science, Stanford University, 1998."},{"key":"10.3166\/ejc.16.624-641_bib0090","series-title":"Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 2993","first-page":"326","article-title":"Benchmarks for hybrid systems verifications","author":"Fehnker","year":"2004"},{"key":"10.3166\/ejc.16.624-641_bib0095","first-page":"172","article-title":"Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems","volume":"21","author":"Fr\u00e4nzle","year":"2008"},{"issue":"5","key":"10.3166\/ejc.16.624-641_bib0100","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Hansson","year":"1994","journal-title":"Form Asp Comput"},{"key":"10.3166\/ejc.16.624-641_bib0105","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.16.624-641_bib0110","series-title":"Quantitative Evaluation of Systems (QEST)","first-page":"243","article-title":"A Markov reward model checker","author":"Katoen","year":"2005"},{"key":"10.3166\/ejc.16.624-641_bib0115","series-title":"Hybrid Systems: Computation and Control, number 3927 in Lecture Notes in Computer Sciences","first-page":"377","article-title":"Computational methods for reachability analysis of stochastic hybrid systems","author":"Koutsoukos","year":"2006"},{"key":"10.3166\/ejc.16.624-641_bib0120","article-title":"Computer-Aided Verification of Coordinating Processes; the Automata-Theoretic Approach","author":"Kurshan","year":"1994","journal-title":"Princeton University Press"},{"key":"10.3166\/ejc.16.624-641_bib0125","series-title":"Numerical Methods for Stochastic Control Problems in Continuous Time","author":"Kushner","year":"2001"},{"key":"10.3166\/ejc.16.624-641_bib0130","series-title":"CONCUR\u201900 number 1877 in Lecture Notes in Computer Sciences","first-page":"123","article-title":"Verifying quantitative properties of continuous probabilistic timed automata","author":"Kwiatkowska","year":"2000"},{"issue":"4","key":"10.3166\/ejc.16.624-641_bib0135","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1109\/TITS.2006.883108","article-title":"Monte Carlo optimization for conict resolution in air traffic control","volume":"7","author":"Lecchini","year":"2006","journal-title":"IEEE Trans Intell Transp Syst"},{"issue":"9","key":"10.3166\/ejc.16.624-641_bib0140","doi-asserted-by":"crossref","first-page":"854","DOI":"10.1109\/TAC.1985.1104071","article-title":"Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system","volume":"30","author":"Malhame","year":"1985","journal-title":"IEEE Trans Autom Control"},{"key":"10.3166\/ejc.16.624-641_bib0145","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.3166\/ejc.16.624-641_bib0150","series-title":"Temporal Verification of Reactive Systems: Safety","author":"Manna","year":"1995"},{"issue":"8","key":"10.3166\/ejc.16.624-641_bib0155","doi-asserted-by":"crossref","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","article-title":"A framework for worstcase and stochastic safety verification using barrier certificates","volume":"52","author":"Prajna","year":"2007","journal-title":"IEEE Trans Autom Control"},{"key":"10.3166\/ejc.16.624-641_bib0160","series-title":"Stochastic hybrid systems, Automation and Control Engineering Series 24","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1201\/9781420008548.ch5","article-title":"Stochastic reachability: Theory and numerical approximation","author":"Prandini","year":"2006"}],"container-title":["European Journal of Control"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0947358010706919?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0947358010706919?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,5]],"date-time":"2018-12-05T00:29:42Z","timestamp":1543969782000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0947358010706919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["S0947358010706919"],"URL":"https:\/\/doi.org\/10.3166\/ejc.16.624-641","relation":{},"ISSN":["0947-3580"],"issn-type":[{"value":"0947-3580","type":"print"}],"subject":[],"published":{"date-parts":[[2010,1]]}}}