{"entities":{"Q2336646":{"pageid":2347389,"ns":120,"title":"Item:Q2336646","lastrevid":57314574,"modified":"2026-03-30T09:37:16Z","type":"item","id":"Q2336646","labels":{"en":{"language":"en","value":"Counterexample-preserving reduction for symbolic model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7131801"}},"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":"Q2336646$BDF3EBA3-DB68-476B-BC36-0233996BA0D0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f3bbd6963fba8c6d01a0ccc92a98a43515c95ead","datavalue":{"value":{"text":"Counterexample-preserving reduction for symbolic model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2336646$61076344-4178-484A-BB65-F50C9686F00D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5c3dbf0ee191d6810a851ffb1698a84912c79da3","datavalue":{"value":"1442.68110","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336646$F9D547A5-1716-481A-99A0-08145D6CD93B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d12127f8c86a02e8aac0553543bb576c5c205994","datavalue":{"value":"10.1155/2014/702165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336646$D385213B-C858-4DBB-84A4-78F3FC6D40CB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"516f52fd1e79844cbe7b2f5aeb3aef6232b4b628","datavalue":{"value":{"entity-type":"item","numeric-id":364385,"id":"Q364385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$0AA9F61E-2A25-4134-AB12-EF745D0237EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"06881a13e9a17045b45f40562997732138d56eb7","datavalue":{"value":{"entity-type":"item","numeric-id":272197,"id":"Q272197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$EDD886BA-DFA5-4429-A8A7-7AED60C91383","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"78e1765f7f48b93959063ee9de183df5d35d45bd","datavalue":{"value":{"entity-type":"item","numeric-id":2336645,"id":"Q2336645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$B1BB389B-5CCE-4E29-BC84-A8DA6089DE59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a987699fd23888733c3cf6186ec5b68180cd27f8","datavalue":{"value":{"entity-type":"item","numeric-id":281290,"id":"Q281290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$06F02373-2571-4CDE-981C-EC2B122D2786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fd40dcc66f818f629fdf5ea0ec1430cc08099ddf","datavalue":{"value":{"entity-type":"item","numeric-id":298500,"id":"Q298500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$70AD326E-EC83-4AC4-B93B-069D75ACD35C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fd013030da45f468fbef74955f8c67832b7b2ff3","datavalue":{"value":{"entity-type":"item","numeric-id":364387,"id":"Q364387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$FAF2562B-AEE8-471D-8D20-A0ACAB3702AF","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":"Q2336646$D4220AC1-AE26-4277-8161-39F4C6F495A1","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":"Q2336646$6A6FF874-66E2-4D09-AE76-0D5F00830CD2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"edb892b5fba668e69aeae77ac9d1c56ac9c86985","datavalue":{"value":"Summary: The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique ``counterexample-preserving reduction'' (CPR, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2336646$F9F65ED4-2B22-4CD3-8BD3-DD4447F65AA4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336646$50C9A4DC-D25F-45F8-B7EB-3747AF4F8CF8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e43ad12564539c1e6b6e6b13c0df6ee851f18e32","datavalue":{"value":"7131801","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336646$08755EE0-DCB0-4284-9D43-7746BE6F5621","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":"Q2336646$87F18D9E-34ED-43C1-820F-FC08876FABB1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ab07118af5dedb57d3c241d372e61485e3378c80","datavalue":{"value":"https://doi.org/10.1155/2014/702165","type":"string"},"datatype":"url"},"type":"statement","id":"Q2336646$B1BA15FE-3856-4D55-A308-BCBE7985EB57","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3ed6e95813d1de657a292f461aac09c3e63aa84a","datavalue":{"value":"W2120106872","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336646$86C7138A-E027-4FCB-AFF0-28833EA37825","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ca5988bee170f044a85367f648d9d9570be066cd","datavalue":{"value":"Q59054119","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2336646$A457A02A-B1BA-4DAF-882E-842EEC19C04F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bc75e886fbdf71be23e2431e3d1861376cec723","datavalue":{"value":{"entity-type":"item","numeric-id":2771059,"id":"Q2771059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$404308C3-4668-427C-9003-5F3CFC422C56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9989385b6d21787669f1b90c6937d74a8a738ea","datavalue":{"value":{"entity-type":"item","numeric-id":5310676,"id":"Q5310676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$67C96D3C-6CD0-46DB-A9A8-F4CE06C3035E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03f882972e0d4020177d8ec9773323d710a3e89a","datavalue":{"value":{"entity-type":"item","numeric-id":3141897,"id":"Q3141897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$FA53481E-4E27-4A2F-91ED-7D9FD51A12EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9a85754f10c794d7ea794155cce4bd2f066956","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$AB5D52C0-0972-4BFD-8501-B0A55DC4C89D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc3406683ad00aa9363d90c4954863b73476c44d","datavalue":{"value":{"entity-type":"item","numeric-id":2843317,"id":"Q2843317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$35B6C2C7-F206-4021-8C9C-AD98ED5C90AA","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":"Q2336646$D5EA21D3-37ED-4A84-B57B-FE73F701DCC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc545c129f526c9b63326a7d44b2e709df1250c4","datavalue":{"value":{"entity-type":"item","numeric-id":4736997,"id":"Q4736997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$25610E59-A91B-4661-8F2A-0D1BA460CFC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"521fcf11de7d8721521e1e478560508699e8a82f","datavalue":{"value":{"entity-type":"item","numeric-id":5492980,"id":"Q5492980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$BE2222B1-DAAD-40BA-A4D4-F3E5999C7BBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77feb9554f98250a94e59cd9498073fd0d68d88e","datavalue":{"value":{"entity-type":"item","numeric-id":5711503,"id":"Q5711503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$4E62D064-0AB5-4AB0-A642-A801F7F02F12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61774d9849f10e1dd86ae551842bcf10d090eb09","datavalue":{"value":{"entity-type":"item","numeric-id":5901905,"id":"Q5901905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$5A2CDEF9-D076-4A0C-AC0C-9A0BF57D780E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26b33d870b8b658fa2258573b1c239cb2fe2b4b5","datavalue":{"value":{"entity-type":"item","numeric-id":4427907,"id":"Q4427907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$90CDC21F-CCE5-4EC8-BC37-803F60A32B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bab9703cb758abcf8ef0a22f113fb1414f37379","datavalue":{"value":{"entity-type":"item","numeric-id":363506,"id":"Q363506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2336646$80046542-1420-4CEC-A057-54A8911C1550","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57c6199eeebd4e12fda339a003e44e534ba50fb3","datavalue":{"value":{"entity-type":"item","numeric-id":2851910,"id":"Q2851910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9dd48b89ab1407d3e25139b8ce3be36d459c7cc6","datavalue":{"value":{"amount":"+0.9682629108428956","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":"Q2336646$4DD4D309-5FA2-44DD-B359-848ED1CBDECA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"052eef5bfe13e7e87b56a0267c03cfd0c3099e2f","datavalue":{"value":{"entity-type":"item","numeric-id":5703781,"id":"Q5703781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37cdfcd4b6e9ed6b8311c26cc8d789528464c9ed","datavalue":{"value":{"amount":"+0.7587806582450867","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":"Q2336646$6F6A06AE-FB0E-4315-9CFC-B8C1B2A653CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c58649780c44d0e6e266dcfe7f7ffd4b10e2f702","datavalue":{"value":{"entity-type":"item","numeric-id":4787241,"id":"Q4787241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da4c1d8ff7e8ac73380b06dea50f779deb0b2281","datavalue":{"value":{"amount":"+0.7573726773262024","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":"Q2336646$830AD817-394B-4871-A6EC-48A4CE893CE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"662f051937086bb2907463bf6ee78e7b61ae81e9","datavalue":{"value":{"entity-type":"item","numeric-id":4493882,"id":"Q4493882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfa0c5ec6a9253d3a186bdc4ba42a18aeb694635","datavalue":{"value":{"amount":"+0.7325872182846069","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":"Q2336646$4D06FC7F-005D-4A55-A0D2-8A7FB0BFE627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf6de32a2dec7b233f9187ef7f7448772352ddbb","datavalue":{"value":{"entity-type":"item","numeric-id":6487557,"id":"Q6487557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfa0c5ec6a9253d3a186bdc4ba42a18aeb694635","datavalue":{"value":{"amount":"+0.7325872182846069","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":"Q2336646$5FBAAD1E-4BFF-43FE-BB5F-8D1C2A142CBB","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":"Q2336646$449453FD-C370-4BFC-A697-E80300C8B3BC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2336646","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2336646"}}}}}