{"entities":{"Q2336669":{"pageid":2347412,"ns":120,"title":"Item:Q2336669","lastrevid":78695600,"modified":"2026-05-06T12:13:15Z","type":"item","id":"Q2336669","labels":{"en":{"language":"en","value":"Terminal satisfiability in GSTE"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7131823"}},"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":"Q2336669$C5710F74-429F-4859-9DB6-30200302E121","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c5d62c4d9ea6ad446ee7f71856d3d68bd25bfa3c","datavalue":{"value":{"text":"Terminal satisfiability in GSTE","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2336669$EFC7AAFE-7AB0-47AE-BFC5-BF2DE31E7D32","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1632feeca7ab9ebc9b64188dcf3fa5638fc2762e","datavalue":{"value":"1442.68111","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336669$F89FF5AD-0C13-497D-9B95-D4434A7EA89C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2338025b2d4450a073018c9258eb80c386170850","datavalue":{"value":"10.1155/2014/725275","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336669$F91D4F75-A584-4F54-945F-010AEF3E3D00","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d4c897416ee20f905d81c0f945e0fc29c92a5a24","datavalue":{"value":{"entity-type":"item","numeric-id":433801,"id":"Q433801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$5D355A2B-82BE-4564-899C-AE12C6CC375F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b992718c0aad0bdb9ac105b054e0fb6e3b3514d4","datavalue":{"value":{"entity-type":"item","numeric-id":2336667,"id":"Q2336667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$CA05074A-47AE-4BF2-BD5A-E9B79FFBD59E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"51d06ede3dcfa197d356ee84f76556911fdf1f29","datavalue":{"value":{"entity-type":"item","numeric-id":2336668,"id":"Q2336668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$F7C69650-3BB4-420E-9331-DD8499ECFAD6","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":"Q2336669$98239EE3-0894-4BE8-B767-B24FFB3CAD86","rank":"normal"},{"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":"Q2336669$669E96C2-2AE1-423D-A0DB-1823F68F34FC","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":"Q2336669$23349873-2B13-4321-A4DE-9AB9F4288D08","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"10393ba55f1a886ba53e75eccd4b56403eff1eb9","datavalue":{"value":{"time":"+2019-11-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2336669$9E14856F-CB70-4E07-AEB9-76859BDB2BFC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"52e9da4849062f1a9d7829e302e6abe5ca5e109e","datavalue":{"value":"Summary: \\textit{Generalized symbolic trajectory evaluation} (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's 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\\times\\) with TMC in the case.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2336669$CC81777A-96D2-4D2E-9158-4496B7278392","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336669$33597632-33CA-4113-ABE3-975D784834D4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0f6a0dc77acec9c9ae3823348fded5cb8ca0bd3f","datavalue":{"value":"7131823","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336669$70A4D2DE-E721-4FDD-BC25-C7442868F8CD","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ce132617671aa0068536dd2c242941e2fbe15947","datavalue":{"value":"Q59052031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336669$FE342F5A-2D0F-4E96-B2A3-ECA500DE555A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$4FC95BB3-EE06-4153-B067-2634EC6FCB21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b792ce763f8f58c8ec463fa21b4c599eb550b3c5","datavalue":{"value":{"entity-type":"item","numeric-id":21448,"id":"Q21448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$A33627AF-39BB-4DFF-B85E-0F10378BEDBB","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":"Q2336669$171E4490-B773-4DC3-ABC6-D0F410CC2C7A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"934b7809db8338c8204e26d1ee09fd6ecd8491dc","datavalue":{"value":"https://doi.org/10.1155/2014/725275","type":"string"},"datatype":"url"},"type":"statement","id":"Q2336669$54F196ED-EE00-4D74-9EA8-ABF03048B755","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4d46db82260aac6169455d3c83be830b85d38dbd","datavalue":{"value":"W2084079064","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336669$2D0AFDEF-1D45-40FD-B6ED-D415ABC24BC6","rank":"normal"}],"P223":[{"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":"Q2336669$2CD907DA-2ACA-4D91-837C-0E647FAA96C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b0c7436976c5b9893e05c1462fed16a80d7904d","datavalue":{"value":{"entity-type":"item","numeric-id":5322945,"id":"Q5322945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$27E5267A-9C65-494D-9746-442F43A67213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b5d4373326ddacd5ad0928810272cc7a23b3585","datavalue":{"value":{"entity-type":"item","numeric-id":5312933,"id":"Q5312933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$D3566617-DED9-47EE-80F3-73C1FD4F7A48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0773f68d76e03445d0ebfcff953ef2cdca72ae2e","datavalue":{"value":{"entity-type":"item","numeric-id":2985888,"id":"Q2985888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$B423573B-48EE-4B83-A126-FFF176AF4C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d01429f6203afa9e4100f19dc26684eeb6bc3720","datavalue":{"value":{"entity-type":"item","numeric-id":3172901,"id":"Q3172901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$09B93562-7961-4B6D-88FC-B248A54E5F5D","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":"Q2336669$52876192-48D1-47B7-AE48-F7023CE6F1AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf4fab5a4519bb0e4a7392865538dc50ad77fca2","datavalue":{"value":{"entity-type":"item","numeric-id":1193587,"id":"Q1193587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$912442FA-12C9-4CD1-AF0F-2A846EF370C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9cdaa2ec8eceac1d3a0c164dd76be4ed6c68bc4d","datavalue":{"value":{"entity-type":"item","numeric-id":5946344,"id":"Q5946344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$D0B3F9BD-732A-405B-9531-DFB0E66C8D9D","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":"4ba5132e0858f1f516a927e9ecaf3423619dadb1","datavalue":{"value":{"amount":"+0.8140347003936768","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":"Q2336669$5C0066F4-9971-4666-9208-DC46F1B14754","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":"a58966fd50cbe0f2f8895b60490ad2af5673c413","datavalue":{"value":{"amount":"+0.7835891842842102","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":"Q2336669$2BAE1659-B91B-4985-A9A6-6A0CCC39136E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d464c276265816ff7bdc9441637291a78957de4e","datavalue":{"value":{"entity-type":"item","numeric-id":5312902,"id":"Q5312902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8323b9d51afed4d66eeadfbe833d2109775f00f2","datavalue":{"value":{"amount":"+0.782265305519104","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":"Q2336669$4F965643-AE89-49F5-8AFC-966176244F21","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":"ac38aef314692caed5caf5d7839e629f47013f4a","datavalue":{"value":{"amount":"+0.7724330425262451","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":"Q2336669$80B4FB26-3162-4E63-A264-810C160AD362","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":"b54bf23e1052efff2400463027a449352a7d3bff","datavalue":{"value":{"amount":"+0.7641044855117798","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":"Q2336669$A837F397-4921-400E-A629-AB1476F07193","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"daf5f856a5d861312ad309ab567540337a5f61d6","datavalue":{"value":{"entity-type":"item","numeric-id":57050,"id":"Q57050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336669$E4B4F247-10A1-4328-949A-84928A1A8B91","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Terminal satisfiability in GSTE","badges":[]}}}}}