{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:58:24Z","timestamp":1729630704487,"version":"3.28.0"},"reference-count":35,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,9]]},"DOI":"10.1109\/dsd.2012.87","type":"proceedings-article","created":{"date-parts":[[2013,1,7]],"date-time":"2013-01-07T14:10:39Z","timestamp":1357567839000},"page":"493-500","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking on Hybrid Automata"],"prefix":"10.1109","author":[{"given":"Alberto","family":"Casagrande","sequence":"first","affiliation":[]},{"given":"Carla","family":"Piazza","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"35","first-page":"51","article-title":"Translating time-course gene expression profiles into semi-algebraic hybrid automata via dimensionality reduction","volume":"4545","author":"casagrande","year":"2007","journal-title":"LNCS"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2007.01.019"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-007-0029-9"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24310-3_19"},{"key":"15","first-page":"136","article-title":"STORMED hybrid systems","volume":"5126","author":"vladimerou","year":"2008","journal-title":"LNCS"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1093\/treephys\/25.10.1303"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2005.1582235"},{"journal-title":"A Calculus of Communicating Systems","year":"1982","author":"milner","key":"13"},{"key":"14","first-page":"324","article-title":"Hybrid automata with finite bisimulations","volume":"944","author":"henzinger","year":"1995","journal-title":"LNCS"},{"journal-title":"Modal Correspondence Theory","year":"1978","author":"van benthem","key":"11"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"21","first-page":"465","article-title":"Series of Abstraction for Hybrid Automata","volume":"2289","author":"tiwari","year":"2002","journal-title":"LNCS"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"23","first-page":"72","article-title":"Construction of Abstract State Graphs with PVS","volume":"1254","author":"graf","year":"1997","journal-title":"LNCS"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(96)00050-1"},{"key":"25","first-page":"686","article-title":"Relational Abstractions for Continuous and Hybrid Systems","volume":"6806","author":"sankaranarayanan","year":"2011","journal-title":"LNCS"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225162"},{"key":"27","first-page":"126","article-title":"Analysis of hybrid systems: An ounce of realism can save an infinity of states","volume":"1683","author":"fra?nzle","year":"1999","journal-title":"LNCS"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-009-0082-7"},{"key":"29","first-page":"74","article-title":"Modularity for timed and hybrid systems","author":"alur","year":"1997","journal-title":"CONCUR'97"},{"key":"3","article-title":"Design and synthesis of synchronization skeletons using brancing time temporal logic","volume":"131","author":"clarke","year":"1981","journal-title":"LNCS"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/235809.235813"},{"key":"1","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BFb0032003","article-title":"From timed to hybrid systems","volume":"600","author":"maler","year":"1991","journal-title":"Real-Time Theory in Practice"},{"key":"30","first-page":"232","article-title":"Lateral Inhibition through Delta-Notch signaling: A Piecewise Affine Hybrid Model","volume":"2034","author":"ghosh","year":"2001","journal-title":"LNCS"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.09.001"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/PL00009858"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"31","first-page":"233","article-title":"Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata","volume":"2623","author":"ghosh","year":"2003","journal-title":"LNCS"},{"key":"4","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","article-title":"Specification and verification of concurrent systems in cesar","author":"queille","year":"1982","journal-title":"Proceedings of the Fifth Colloquium on International Symposium on Programming"},{"key":"9","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","author":"tarski","year":"1951","journal-title":"A decision method for elementary algebra and geometry"},{"journal-title":"Introduction to Mathematical Logic","year":"1997","author":"mendelson","key":"8"}],"event":{"name":"2012 15th Euromicro Conference on Digital System Design (DSD)","start":{"date-parts":[[2012,9,5]]},"location":"Cesme, Izmir, Turkey","end":{"date-parts":[[2012,9,8]]}},"container-title":["2012 15th Euromicro Conference on Digital System Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6384916\/6386869\/06386932.pdf?arnumber=6386932","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,5]],"date-time":"2022-02-05T08:34:02Z","timestamp":1644050042000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6386932\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1109\/dsd.2012.87","relation":{},"subject":[],"published":{"date-parts":[[2012,9]]}}}