{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T04:51:56Z","timestamp":1648702316330},"reference-count":19,"publisher":"Hindawi Limited","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["60973016","61272175","2010CB328004","SGSCDK00DWKJ1300510"],"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":[[2014]]},"abstract":"Generalized symbolic trajectory evaluation<\/jats:italic>(GSTE) is an extension of symbolic trajectory evaluation (STE) and a method of model checking. GSTE specifications are given as assertion graphs. There are four efficient methods to verify whether a circuit model obeys an assertion graph in GSTE, Model Checking Strong Satisfiability (SMC), Model Checking Normal Satisfiability (NMC), Model Checking Fair Satisfiability (FMC), and Model Checking Terminal Satisfiability (TMC). SMC, NMC, and FMC have been proved and applied in industry, but TMC has not. This paper gives a six-tuple definition and presents a new algorithm for TMC. Based on these, we prove that our algorithm is sound and complete. It solves the SMC\u2019s limitation (resulting in false negative) without extending from finite specification to infinite specification. At last, a case of using TMC to verify a realistic hardware circuit round-robin arbiter is achieved. Avoiding verifying the undesired paths which are not related to the specifications, TMC makes it possible to reduce the computational complexity, and the experimental results suggest that the time cost by SMC is 3.14\u00d7 with TMC in the case.<\/jats:p>","DOI":"10.1155\/2014\/725275","type":"journal-article","created":{"date-parts":[[2014,5,15]],"date-time":"2014-05-15T21:09:56Z","timestamp":1400188196000},"page":"1-10","source":"Crossref","is-referenced-by-count":0,"title":["Terminal Satisfiability in GSTE"],"prefix":"10.1155","volume":"2014","author":[{"given":"Yongsheng","family":"Xu","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, Sichuan 611731, China"}]},{"given":"Guowu","family":"Yang","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, Sichuan 611731, China"}]},{"given":"Zhengwei","family":"Chang","sequence":"additional","affiliation":[{"name":"State Grid Sichuan Electric Power Research Institute, Chengdu, Sichuan 610000, China"}]},{"given":"Desheng","family":"Zheng","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, Sichuan 611731, China"}]},{"given":"Wensheng","family":"Guo","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, Sichuan 611731, China"}]}],"member":"98","reference":[{"key":"1","year":"1999"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/43.372367"},{"key":"3","first-page":"3","volume-title":"Symbolic trajectory evaluation","year":"1997"},{"key":"4","first-page":"411","volume-title":"Pvs: combining specification, proof checking, and model checking","year":"1996"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383966"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/43.771176"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2003.812320"},{"key":"9","first-page":"176","volume-title":"Progress on the state explosion problem in model checking","year":"2001"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_19"},{"key":"11","year":"2008"},{"key":"12","first-page":"143","volume-title":"Efficient model checking using tabled resolution","year":"1997"},{"key":"13","first-page":"479","volume-title":"Mck: model checking the logic of knowledge","year":"2004"},{"key":"16","first-page":"1","volume-title":"Statistical model checking for cyber-physical systems","year":"2011"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"19","first-page":"170","volume-title":"Reasoning about gste assertion graphs","year":"2003"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"21","first-page":"118","volume":"58","year":"2003","journal-title":"Advances in Computers"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/725275.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/725275.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/725275.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,7,29]],"date-time":"2016-07-29T06:22:09Z","timestamp":1469773329000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2014\/725275\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":19,"alternative-id":["725275","725275"],"URL":"https:\/\/doi.org\/10.1155\/2014\/725275","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"value":"1110-757X","type":"print"},{"value":"1687-0042","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}