{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:46Z","timestamp":1740134566767,"version":"3.37.3"},"reference-count":15,"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\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["60973016","61272175","2010CB328004"],"award-info":[{"award-number":["60973016","61272175","2010CB328004"]}],"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":["60973016","61272175","2010CB328004"],"award-info":[{"award-number":["60973016","61272175","2010CB328004"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012166","name":"National Basic Research Program of China","doi-asserted-by":"crossref","award":["60973016","61272175","2010CB328004"],"award-info":[{"award-number":["60973016","61272175","2010CB328004"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2013]]},"abstract":"<jats:p>Generalized symbolic trajectory evaluation (GSTE) is a model checking approach and has successfully demonstrated its powerful capacity in formal verification of VLSI systems. GSTE is an extension of symbolic trajectory evaluation (STE) to the model checking of<mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" id=\"M1\"><mml:mrow><mml:mi>\u03c9<\/mml:mi><\/mml:mrow><\/mml:math>-regular properties. It is an alternative to classical model checking algorithms where properties are specified as finite-state automata. In GSTE, properties are specified as assertion graphs, which are labeled directed graphs where each edge is labeled with two labeling functions: antecedent and consequent. In this paper, we show the complement relation between GSTE assertion graphs and finite-state automata with the expressiveness of regular languages and<mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" id=\"M2\"><mml:mrow><mml:mi>\u03c9<\/mml:mi><\/mml:mrow><\/mml:math>-regular languages. We present an algorithm that transforms a GSTE assertion graph to a finite-state automaton and vice versa. By applying this algorithm, we transform the problem of GSTE assertion graphs implication to the problem of automata language containment. We demonstrate our approach with its application to verification of an FIFO circuit.<\/jats:p>","DOI":"10.1155\/2013\/709071","type":"journal-article","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T21:02:07Z","timestamp":1373490127000},"page":"1-7","source":"Crossref","is-referenced-by-count":0,"title":["A Transformation-Based Approach to Implication of GSTE Assertion Graphs"],"prefix":"10.1155","volume":"2013","author":[{"given":"Guowu","family":"Yang","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology Chengdu, Sichuan 610054, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William N. N.","family":"Hung","sequence":"additional","affiliation":[{"name":"Synopsys Inc., Mountain View, CA 94043, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[{"name":"Department of ECE, Portland State University, Portland, Oregon, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wensheng","family":"Guo","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology Chengdu, Sichuan 610054, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"2","first-page":"70","volume-title":"Generalized symbolic trajectory evaluation-abstraction in action","volume":"2517","year":"2002"},{"doi-asserted-by":"publisher","key":"3","DOI":"10.1109\/TVLSI.2003.812320"},{"key":"4","first-page":"216","volume-title":"Compositional specification and model checking in GSTE","volume":"3114","year":"2004"},{"volume-title":"High level validation of next generation microprocessors","year":"2002","key":"5"},{"doi-asserted-by":"publisher","key":"8","DOI":"10.1007\/3-540-48683-6_19"},{"doi-asserted-by":"publisher","key":"9","DOI":"10.1007\/BF01383966"},{"volume-title":"Finding bugs in an \u03b1 microprocessor using satisfiability solvers","year":"2001","first-page":"454","key":"11"},{"volume-title":"Formal verification of a superscalar execution unit","year":"1997","first-page":"161","key":"12"},{"doi-asserted-by":"publisher","key":"15","DOI":"10.1007\/978-3-540-27813-9_18"},{"doi-asserted-by":"publisher","key":"19","DOI":"10.1016\/0022-0000(87)90036-5"},{"volume-title":"Complementation is more difficult with automata on infinite words","year":"1988","key":"20"},{"volume-title":"On the complexity of omega-automata","year":"1988","first-page":"319","key":"21"},{"volume-title":"On a decision method in restricted second order arithmetic","year":"1962","first-page":"1","key":"23"},{"volume-title":"Verifying vhdl designs with cospan","year":"1997","first-page":"206","key":"24"},{"year":"1994","series-title":"Princeton Series in Computer Science","key":"25"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/709071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/709071.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/709071.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,8]],"date-time":"2020-05-08T17:56:29Z","timestamp":1588960589000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2013\/709071\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":15,"alternative-id":["709071","709071"],"URL":"https:\/\/doi.org\/10.1155\/2013\/709071","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2013]]}}}