{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T21:58:52Z","timestamp":1783115932897,"version":"3.54.6"},"reference-count":10,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2003,8]]},"abstract":"<jats:p> Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods. <\/jats:p>","DOI":"10.1142\/s012905410300190x","type":"journal-article","created":{"date-parts":[[2003,9,19]],"date-time":"2003-09-19T06:19:32Z","timestamp":1063952372000},"page":"583-604","source":"Crossref","is-referenced-by-count":127,"title":["Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems"],"prefix":"10.1142","volume":"14","author":[{"given":"Edmund","family":"Clarke","sequence":"first","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ansgar","family":"Fehnker","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhi","family":"Han","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruce","family":"Krogh","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olaf","family":"Stursberg","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15213, USA"},{"name":"Process Control Lab (CT-AST), University of Dortmund, 44221 Dortmund, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Theobald","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"rf5","volume":"36","author":"Ball T.","journal-title":"PLDI"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1109\/9.948467"},{"key":"rf12","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"rf23","volume-title":"G\u00f6del, Escher, Bach: An Eternal Golden Braid","author":"Hofstadter D. R.","year":"1989"},{"key":"rf24","series-title":"LNCS","volume-title":"Static Analysis Symposium","volume":"1694","author":"Jeannet B.","year":"1999"},{"key":"rf25","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"Kurshan R.","year":"1994"},{"key":"rf26","unstructured":"A.\u00a0Kurzhanski and P.\u00a0Varaiya, HSCC, LNCS\u00a01790 (Springer, 2000)\u00a0pp. 203\u2013213."},{"key":"rf27","unstructured":"G.\u00a0Lafferriere, G.J.\u00a0Pappas and S.\u00a0Yovine, HSCC, LNCS\u00a01569 (Springer, 1999)\u00a0pp. 103\u2013116."},{"key":"rf30","doi-asserted-by":"crossref","unstructured":"A.\u00a0Tiwari and G.\u00a0Khanna, HSCC, LNCS\u00a02289 (Springer, 2002)\u00a0pp. 465\u2013478.","DOI":"10.1007\/3-540-45873-5_36"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S012905410300190X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T20:37:55Z","timestamp":1565123875000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S012905410300190X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":10,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2003,8]]}},"alternative-id":["10.1142\/S012905410300190X"],"URL":"https:\/\/doi.org\/10.1142\/s012905410300190x","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}