{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:39:32Z","timestamp":1761647972407},"reference-count":25,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Sci. Eng."],"published-print":{"date-parts":[[2013,1]]},"DOI":"10.1109\/tase.2012.2198917","type":"journal-article","created":{"date-parts":[[2012,6,14]],"date-time":"2012-06-14T19:38:01Z","timestamp":1339702681000},"page":"160-170","source":"Crossref","is-referenced-by-count":4,"title":["Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata With Variables"],"prefix":"10.1109","volume":"10","author":[{"given":"Changyan","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ratnesh","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1145\/157485.164585","article-title":"automatic functional test generation using the extended finite state machine model","author":"cheng","year":"1993","journal-title":"30th ACM\/IEEE Design Automation Conference"},{"key":"ref11","first-page":"72","article-title":"Construction of abstract state graphs with PVS","volume":"1254","author":"graf","year":"1997","journal-title":"Proc Conf Computer-Aided Verification (CAV)"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(01)00008-9"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042039"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_28"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2006.1657692"},{"key":"ref18","first-page":"50","article-title":"Symbolic transition graph with assignment","author":"lin","year":"1996","journal-title":"Proc CONCUR"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384313"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","article-title":"Bebop: A symbolic model checker for boolean programs","volume":"1885","author":"ball","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.003"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72734-7_6"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref9","first-page":"400","article-title":"Symbolic model checking of infinite state systems using presburger arithmetic","author":"bultan","year":"1997","journal-title":"Proc CAV"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"ref20","doi-asserted-by":"crossref","DOI":"10.21236\/ADA196047","author":"lynch","year":"1988","journal-title":"I\/O automata a model for discrete event systems"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2003.1272635"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/BFb0014555","article-title":"Local model checking for value-passing processes","author":"rathke","year":"1997","journal-title":"Proc Int Symp Theor Aspects Comput Softw (TACS'97)"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCB.2003.811516"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2004.838497"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2009.5160198"}],"container-title":["IEEE Transactions on Automation Science and Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8856\/6387323\/06218131.pdf?arnumber=6218131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,30]],"date-time":"2019-06-30T00:38:51Z","timestamp":1561855131000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6218131\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":25,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tase.2012.2198917","relation":{},"ISSN":["1545-5955","1558-3783"],"issn-type":[{"value":"1545-5955","type":"print"},{"value":"1558-3783","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}