{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:47Z","timestamp":1740134567155,"version":"3.37.3"},"reference-count":25,"publisher":"Wiley","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/501100012164","name":"863 Program","doi-asserted-by":"crossref","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100012164","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012164","name":"863 Program","doi-asserted-by":"crossref","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100012164","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004602","name":"Program for New Century Excellent Talents in University","doi-asserted-by":"publisher","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100004602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"],"award-info":[{"award-number":["2011AA010106","2012AA011201","61120106006","91118007","61133007","61272335","61103012"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2013]]},"abstract":"<jats:p>As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic. In this paper, we present a semantic BMC encoding approach to deal with the mixture of<mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" id=\"M1\"><mml:mrow><mml:msub><mml:mrow><mml:mtext>ETL<\/mml:mtext><\/mml:mrow><mml:mrow><mml:mi>f<\/mml:mi><\/mml:mrow><\/mml:msub><\/mml:mrow><\/mml:math>and<mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" id=\"M2\"><mml:mrow><mml:msub><mml:mrow><mml:mtext>ETL<\/mml:mtext><\/mml:mrow><mml:mrow><mml:mi>l<\/mml:mi><\/mml:mrow><\/mml:msub><\/mml:mrow><\/mml:math>. Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it. The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.<\/jats:p>","DOI":"10.1155\/2013\/462532","type":"journal-article","created":{"date-parts":[[2013,7,14]],"date-time":"2013-07-14T21:02:35Z","timestamp":1373835755000},"page":"1-12","source":"Crossref","is-referenced-by-count":2,"title":["Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives"],"prefix":"10.1155","volume":"2013","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5913-4351","authenticated-orcid":true,"given":"Rui","family":"Wang","sequence":"first","affiliation":[{"name":"College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2315-1704","authenticated-orcid":true,"given":"Wanwei","family":"Liu","sequence":"additional","affiliation":[{"name":"College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7498-3909","authenticated-orcid":true,"given":"Tun","family":"Li","sequence":"additional","affiliation":[{"name":"College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4204-7424","authenticated-orcid":true,"given":"Xiaoguang","family":"Mao","sequence":"additional","affiliation":[{"name":"College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":true,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, China"}]}],"member":"311","reference":[{"issue":"8","key":"7","first-page":"677","volume":"35","year":"1986","journal-title":"IEEE Transactions on Computers C"},{"key":"5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Symbolic model checking without BDDs","volume":"1579","year":"1999"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015727"},{"key":"3","series-title":"Lecture Notes in Computer Science","first-page":"62","volume-title":"Temporal logic with fixed points","volume":"398","year":"1987"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-540-75292-9_20","volume-title":"Regular linear temporal logic","volume":"4711","year":"2007"},{"key":"2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"The ForSpec temporal logic: a new temporal property-specification language","volume":"2280","year":"2002"},{"key":"4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"The temporal logic sugar","volume":"2102","year":"2001"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.3724\/SP.J.1001.2009.03449"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-009-0003-9"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.07.016"},{"key":"25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/11813040_38","volume":"4085","year":"2006","journal-title":"Formal Methods"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.19"},{"key":"12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Another look at LTL model checking","volume":"818","year":"1994"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-540-30494-4_14","volume-title":"Simple bounded LTL model checking","volume":"3312","year":"2004"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_25"},{"key":"14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Incremental and complete bounded model checking for full PLTL","volume":"3576","year":"2005"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(1:5)2008"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/377978.377993"},{"key":"13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-540-30476-0_10","volume-title":"B\u00fcchi complementation made tighter","volume":"3299","year":"2004"},{"key":"26","first-page":"661","volume-title":"B\u00fcchi complementation made tight","volume":"3","year":"2009"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/462532.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/462532.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/462532.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,8]],"date-time":"2020-05-08T18:06:23Z","timestamp":1588961183000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2013\/462532\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":25,"alternative-id":["462532","462532"],"URL":"https:\/\/doi.org\/10.1155\/2013\/462532","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2013]]}}}