{"entities":{"Q364478":{"pageid":366245,"ns":120,"title":"Item:Q364478","lastrevid":61270896,"modified":"2026-04-10T22:16:56Z","type":"item","id":"Q364478","labels":{"en":{"language":"en","value":"A transformation-based approach to implication of GSTE assertion graphs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6206842"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$CCC4617A-D5CE-440C-8E3F-C05F31218850","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0feb981c682e975b95bad7d036eb5bc42f4a52c6","datavalue":{"value":{"text":"A transformation-based approach to implication of GSTE assertion graphs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q364478$095C0BC3-B6B2-4832-A0B0-27D6082BD2D1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2fae36cc162666957d7e87fb21cc3eb99e89f79e","datavalue":{"value":"1311.68091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$298B581B-0722-4552-8698-FC94CE3C853A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3b913dd5610dffdb5c7295f9b48ee2e30226c08c","datavalue":{"value":"10.1155/2013/709071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$4AB5FC83-7DD6-4750-A80D-BFE4C6BFA366","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"919e6c3d25d4b31af34f9da4d9d9f2b8c84ebfe3","datavalue":{"value":{"entity-type":"item","numeric-id":293936,"id":"Q293936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$E5EC7A6A-19B3-4A27-97AF-4301C7641F5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1caedec2f74947a2d17e2400cfb77f2b4f640d20","datavalue":{"value":{"entity-type":"item","numeric-id":364475,"id":"Q364475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$01B124EF-D395-4437-AF6B-F254279A5300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07abc0868bbf3c0352f8089c12b27e770f5814c5","datavalue":{"value":{"entity-type":"item","numeric-id":364476,"id":"Q364476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$24277EF5-C7CD-437A-899B-051E3A75E62D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb7ed5f00aedc28fd11ee0b18554123ae538b561","datavalue":{"value":{"entity-type":"item","numeric-id":364477,"id":"Q364477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$CEB84F57-7E7B-47A8-951A-B3FA5A991605","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$A4015101-66E1-4BEE-B05D-388949F6156E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6e8c017497806797f217f1d658e3d224a2498206","datavalue":{"value":{"time":"+2013-09-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q364478$3D7BE04B-D2EF-4548-A472-596933377051","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5712443d40b7a3dc61642541c3d89c700c1b3d7f","datavalue":{"value":"Summary: 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 \\(\\omega\\)-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 \\(\\omega\\)-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.","type":"string"},"datatype":"string"},"type":"statement","id":"Q364478$4431541C-DF8A-470F-A3B2-ACB406129E8A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$EA42F6F0-C66D-4BDC-85B8-517052C14290","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$EE4B4AFC-203F-4552-8B03-E378076D91A3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"af4f7dcb4e924f0d6189bd8860ad8b00263d404f","datavalue":{"value":"6206842","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$A2A18589-9F20-4999-B916-7970A95870CB","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ff7d1e7f328da9b79b1509975b7c08c622701b98","datavalue":{"value":"Q59003906","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$9DA7964A-EF1C-4828-86AE-FB8AC80F56D2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$BE5D3756-4B48-466B-887B-BB930F906EA6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ece7dd48dcb5e736dd7770359c2a42d600c7405","datavalue":{"value":"https://doi.org/10.1155/2013/709071","type":"string"},"datatype":"url"},"type":"statement","id":"Q364478$16AF51B1-E786-4137-BD06-DE3709585E70","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3dd0524d7cded0f7fe5fb25d852c91e9218a29db","datavalue":{"value":"W1994745936","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$66F22EDE-B694-474B-8446-8038AA8620FA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8337a02542987fb094141aea7282e71631613387","datavalue":{"value":{"entity-type":"item","numeric-id":4427896,"id":"Q4427896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$BC909BFC-521E-4925-BD4C-CF77C7369B48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a30cc351ca06556fd78f196b89cfbe96cc266934","datavalue":{"value":{"entity-type":"item","numeric-id":5312901,"id":"Q5312901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$AEE41AE2-B165-4C53-87EE-5FBA3CF1C2EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44120d819fbc0dc306d919ce7fe009636ee62efc","datavalue":{"value":{"entity-type":"item","numeric-id":5897066,"id":"Q5897066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$C5AB972D-36C2-43E0-A8E9-A56352F7902B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0dd09b3fecfbd3fb9f542f7c1e52e3df257f2b9","datavalue":{"value":{"entity-type":"item","numeric-id":4817544,"id":"Q4817544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$4D844B8F-AAE2-4A41-9BF0-35F16D022C43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3199ee993e7659b1e87a4f739fb4a0238b116c7f","datavalue":{"value":{"entity-type":"item","numeric-id":4553262,"id":"Q4553262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$3AB00E11-83F6-4C31-BEC5-E73B4E46B0F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41c258e920b69fc9081ac0baf8648a0039856b1c","datavalue":{"value":{"entity-type":"item","numeric-id":5312902,"id":"Q5312902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$56E286C8-DDCC-4CC1-B5AF-A41F1E7CF7B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"befac40fe1cb8125522cebeee5546ac3f483c4d3","datavalue":{"value":{"entity-type":"item","numeric-id":5394176,"id":"Q5394176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$2A0EF98F-E533-413F-8DA8-7CD2EC1ECA26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ce8f46c76b70725b31c46e21e48547b8f386e27","datavalue":{"value":{"entity-type":"item","numeric-id":5308436,"id":"Q5308436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$A49406E3-1D50-4889-B21E-3D9C69373BAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab4573b227fbba8ffa410ea5afa5ff5132abb7d","datavalue":{"value":{"entity-type":"item","numeric-id":1116702,"id":"Q1116702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$19B1401C-25DA-45D4-8314-CECA405FF9D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06c411f40bd3fed70a734570dda325013084ac01","datavalue":{"value":{"entity-type":"item","numeric-id":5525343,"id":"Q5525343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$DDB05258-F058-489E-AE4E-5208CDFD7DB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f60db55428521e0cf5ccdeaa2bf5e3fd0ed1e94","datavalue":{"value":{"entity-type":"item","numeric-id":4326390,"id":"Q4326390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$32C5932B-4798-4480-A894-45AF7CFE68E5","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"2d5ee5346cabfffc57c943bd941ca2a4ac1a2a9a","datavalue":{"value":"journals/jam/YangHSG13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364478$610A8D7F-7760-4CCF-B181-8D28F362EDB4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353c608691c01000aeeb208adf4492bc17b2a88d","datavalue":{"value":{"entity-type":"item","numeric-id":5897066,"id":"Q5897066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a192baf9d6206b8521444f32af596f3c213e7af","datavalue":{"value":{"amount":"+0.8631635904312134","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q364478$1332AF9F-014F-4E1D-B989-6C56E4073844","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"124f67889e8bbd9aa673433a181b944c636f9cf3","datavalue":{"value":{"entity-type":"item","numeric-id":3636800,"id":"Q3636800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bffe38fdd6fb3a4a3a69835312ac6b262b181bd7","datavalue":{"value":{"amount":"+0.7726727724075317","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q364478$51E0E7D6-E0DC-4758-9B72-76D88C87DBA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c06c91ccc34184c97e64bdd0a94d2a8fce943aa7","datavalue":{"value":{"entity-type":"item","numeric-id":4427896,"id":"Q4427896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d7ccc3e8c2842ace5189860def5db95ca1b8d15","datavalue":{"value":{"amount":"+0.7685807347297668","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q364478$5A2F7C71-907F-4E23-9612-040B8CFBE3F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e279f9e0b086d6b3b8f18b8a3d2df0a7cb3ea1c9","datavalue":{"value":{"entity-type":"item","numeric-id":5898920,"id":"Q5898920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d275544d18a7f87623a6f43c4a47093b401dfe02","datavalue":{"value":{"amount":"+0.7660542130470276","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q364478$AFBC40DE-A9B0-4499-B073-CB661357EE88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bffe8dbffeedd3a5bbdba52b07669a1c7cd1cc1","datavalue":{"value":{"entity-type":"item","numeric-id":2385196,"id":"Q2385196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e23e603f299e4453f33fa8cf47d1b63f79b978cc","datavalue":{"value":{"amount":"+0.752280592918396","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q364478$76997A8D-4B95-4D01-B377-7EF82ECBC5E3","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364478$B27202BB-6276-467C-82F0-D9A8D68CBC75","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A transformation-based approach to implication of GSTE assertion graphs","badges":[]}}}}}