{"entities":{"Q690465":{"pageid":692314,"ns":120,"title":"Item:Q690465","lastrevid":63650508,"modified":"2026-04-11T14:36:52Z","type":"item","id":"Q690465","labels":{"en":{"language":"en","value":"An efficient approach for abstraction-refinement in model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6110691"}},"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":"Q690465$12FCAE38-7506-4534-91E9-85A469839DEF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"08430c48ad32a1389fed84e98f51c086eb0687d3","datavalue":{"value":{"text":"An efficient approach for abstraction-refinement in model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q690465$E826C094-D21B-497E-BAEE-EF9BCDA07F40","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f5c739324093b9db2160b7d2649b285c7824e90a","datavalue":{"value":"1252.68197","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690465$11EBB5AB-03CC-4199-AD50-5D4CE38D94BB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b63c8a7d27ac589b244a048d2f920a9e8c6bd330","datavalue":{"value":{"entity-type":"item","numeric-id":247892,"id":"Q247892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$9A06B013-BAE7-4258-A476-A58CE01C2645","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"30d9aa89bda10e60a2b2b6e5c4297a8a726a7ab3","datavalue":{"value":{"entity-type":"item","numeric-id":247891,"id":"Q247891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$830E0A53-9B50-4DB9-93ED-50DFF716DF34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"83e0c9ae8671e5f29856e35bbe5db8cbb2ecbb5c","datavalue":{"value":{"entity-type":"item","numeric-id":247888,"id":"Q247888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$B050EFE6-D3C6-4684-9E42-BE7A0857AF61","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$4A049436-9DAC-47B1-B881-0FE5AA398778","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"95e36ecb600c934bbc19d79b7ffc96af390338f1","datavalue":{"value":{"time":"+2012-11-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q690465$C8DB956F-C4D9-4EEB-9017-376C92B794E5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690465$6D79F832-BD43-43AC-8058-7B2C2E7A0161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690465$8AC6B39D-FA31-45AB-8B1B-11DAB440D9A3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"03a7dbac6d83ecfe5c0c450ef2197437e952c937","datavalue":{"value":"6110691","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690465$E2DB87D3-7E58-414F-B91C-9278B0C73EC9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q690465$9DEC3EEC-B2F2-4A79-8D20-F92A0BF1705C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q690465$29521833-00E6-4A10-B5E0-11EDC66A3AC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e404e0d47002bfb1532cb42cfe324606a2151619","datavalue":{"value":"abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q690465$39CA58CD-9467-4CF8-95AB-C6098F9BF39E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab20a0363e682206851b94b3be1e96bb56399f58","datavalue":{"value":"refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q690465$1F982358-27EE-47E0-B1B6-BF0CA6331271","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48ddf43eca498c7e7087cd696beb82ea63925320","datavalue":{"value":"algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q690465$2CC4FD8C-91EF-4B89-810F-15AC612A8D00","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f078e243cc5b2a268355ae913e6ed1ca3bb0dc8","datavalue":{"value":{"entity-type":"item","numeric-id":20519,"id":"Q20519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$713ADDEB-3D42-4729-8D39-AB1B97441F35","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":"Q690465$C14D2038-BCBA-4626-83E6-82CECE8E35C8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"09880a7d3d9ed0e8d61e59a5043e7f473fc07ac8","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2011.12.014","type":"string"},"datatype":"url"},"type":"statement","id":"Q690465$2546728D-D6CA-4072-B5B8-A2D7E2349401","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"48dbfca4f5882be2a2198bfdf0e74eaec1f8df02","datavalue":{"value":"W2069919327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690465$F8D24BF6-3CF1-4CC6-8C1E-2386ECB08EDC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"90e44ff29e928f19b892ec1c13836498e6c5624c","datavalue":{"value":{"entity-type":"item","numeric-id":3512441,"id":"Q3512441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$7A419321-A170-4963-81BF-4CDA1BCBFAF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7cd2a25d693a4acd921e56f15d1b3d06cb750f8","datavalue":{"value":{"entity-type":"item","numeric-id":2754081,"id":"Q2754081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$1B86BE2B-B795-48E9-8556-6347983D5C12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fe5bbcf5918492c7dfe6244e9597e637230da0b","datavalue":{"value":{"entity-type":"item","numeric-id":5728442,"id":"Q5728442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$10525702-E286-4AD0-8180-7F4A5993EA41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a38492a2d29ca2079d3ea6fef3f6b16bf3406a4f","datavalue":{"value":{"entity-type":"item","numeric-id":5280833,"id":"Q5280833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$B8461F0B-9E1A-4A99-A5E7-93EC0713803B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30d8dc0d538f37be56fd0251f11c2dbcbf4aa0f4","datavalue":{"value":{"entity-type":"item","numeric-id":2817629,"id":"Q2817629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$5F023F84-5E40-4FA5-A0FF-65A2D83BFBFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52399dbd6e9bc23018f1172efb05b548b6e91780","datavalue":{"value":{"entity-type":"item","numeric-id":4804901,"id":"Q4804901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$954EE5B4-DA7C-40C4-92D9-BE31D51C4143","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb19e18c12ddea2b553dcb695cb9473546265295","datavalue":{"value":{"entity-type":"item","numeric-id":4427894,"id":"Q4427894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$9F8005C3-B489-4F90-AD43-AC23CDC28789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c21e537ab0c07b0d3849b9a7e5a291ced75540","datavalue":{"value":{"entity-type":"item","numeric-id":5178898,"id":"Q5178898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$6E38736B-8A2D-427C-8214-E4F42B93E0D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e4de8e02463aa9adeead8bdc6d0fc6c098b1202","datavalue":{"value":{"entity-type":"item","numeric-id":4417922,"id":"Q4417922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690465$E0BCA720-76BE-49AE-A844-D1ADDE12D77F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f38dfd666009cefca45391a9d54ed79e1cb8a061","datavalue":{"value":"10.1016/J.TCS.2011.12.014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690465$69F3C32E-D3F2-478A-A786-4E9507D96734","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9f89c2bc27eef1cdb709afd3f818dfc87424f5d0","datavalue":{"value":{"entity-type":"item","numeric-id":3087967,"id":"Q3087967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53f715186cb835b9e43e0225402475d7ac9a4bc4","datavalue":{"value":{"amount":"+0.98374116","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$84DB917F-D4B3-4957-BA59-D003BA29662D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e360b6e95f407b30484300ceaa660de75a99d81d","datavalue":{"value":{"entity-type":"item","numeric-id":5435632,"id":"Q5435632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0201e2f2f3fcd1fcb8801b08eb1e2773f5feaf69","datavalue":{"value":{"amount":"+0.96802115","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$681CD9B0-81F9-40F3-B415-FC7EC0A0A609","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b3630aac79ff9218da345a9db86dee931ca6a02","datavalue":{"value":{"entity-type":"item","numeric-id":3591392,"id":"Q3591392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26de23270d38c431fc5ecb6c3f1c12493fed7213","datavalue":{"value":{"amount":"+0.9662561","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$8CF3D0D4-AF8B-4F8A-87CA-57D2D0AB97BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0dbb9ce060d55e1b403f2129112efe14249c6bae","datavalue":{"value":{"entity-type":"item","numeric-id":2845512,"id":"Q2845512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0aa54eee629dd39e5a4ddd51f9ae4d1e0cad98da","datavalue":{"value":{"amount":"+0.9639929","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$DF11BC3B-3E3B-4DA0-AEBF-275B2B944F02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b9fc369e46fc329463fea3bac110c1110bcfcc7","datavalue":{"value":{"entity-type":"item","numeric-id":5716541,"id":"Q5716541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dd32572f228d79dcef4a6455de85c3405075120","datavalue":{"value":{"amount":"+0.95642006","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$63316410-D6E9-4C5A-A2E6-4985FB102CB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61edb7ecab1f5627dc9d20ac76c9e88dd4557c3a","datavalue":{"value":{"entity-type":"item","numeric-id":4923520,"id":"Q4923520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82b3eff083e12d52d168034dd4b639bf1ca68e6f","datavalue":{"value":{"amount":"+0.95152617","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$2BC02131-1B39-4D08-AA66-6AC439DF9358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b09e2fecb0c07b29b5d6d381a95c3ad04f26318","datavalue":{"value":{"entity-type":"item","numeric-id":5394185,"id":"Q5394185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4eda2557efcc402b453908041bc0087e3d85cdcb","datavalue":{"value":{"amount":"+0.95073485","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$72BFA352-786A-450A-97C5-C61790FABE32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dce5cfd9f03d9a0ba61f291e4026b26bede70abc","datavalue":{"value":{"entity-type":"item","numeric-id":4823139,"id":"Q4823139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"abacd4a9ffac93e34cb90f006372ab66d88cf97b","datavalue":{"value":{"amount":"+0.944185","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$09C94299-6DB7-4114-A2E6-90ED47E238D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edc30b245ec6b807d4e24f0d259d8f49ecc3c7a9","datavalue":{"value":{"entity-type":"item","numeric-id":5758121,"id":"Q5758121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31cc0772f22f944280f6dbf397d159275f3de5e0","datavalue":{"value":{"amount":"+0.93485016","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690465$0CF47CBD-A749-4564-9962-B760146E9960","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An efficient approach for abstraction-refinement in model checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_efficient_approach_for_abstraction-refinement_in_model_checking"}}}}}