{"entities":{"Q5222973":{"pageid":7252543,"ns":120,"title":"Item:Q5222973","lastrevid":41188130,"modified":"2025-04-18T21:17:55Z","type":"item","id":"Q5222973","labels":{"en":{"language":"en","value":"Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7076883"}},"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":"Q5222973$514CC8A4-8BD0-4AE0-AD34-75FFACD8C2A0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d73cbb7395e3652e2b8971450f039eca0dbf9a1b","datavalue":{"value":{"text":"Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5222973$77F37B5B-098A-486C-A9C2-6630F23FBEC6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae5bcfae9d5ed097b07cfa768e542646b57b1bef","datavalue":{"value":"1415.68149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222973$37191CC2-FD14-403A-A0DB-50E1A7CFA7B7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"aa2fab7114b715c2524682a9493c3f0a5808f53e","datavalue":{"value":{"entity-type":"item","numeric-id":2324219,"id":"Q2324219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222973$17CB2462-0CC4-4951-B4C0-927C588711CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f4a9452230b48b25729b39bc47037fb4f65b446","datavalue":{"value":{"entity-type":"item","numeric-id":2158284,"id":"Q2158284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222973$02F8C005-0035-49AD-B5B1-B67B50052EFD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eae4601ff702bcaa610b94b3434abd8165930c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4645721,"id":"Q4645721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222973$75E9632E-3963-4217-9201-9119132E8671","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"311afef0a4b95245df7f6c2908ad6e9d40f3f2be","datavalue":{"value":{"time":"+2019-07-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5222973$83B290F0-CDCF-4496-ABCF-A7CF9E394A53","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222973$C2B99D8C-04E7-443F-93DE-C68DDEB081AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222973$1E19390C-B053-4DE8-A224-B929CADFE894","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"215c2e1d448c2aa689dc127a25730d2ed7225139","datavalue":{"value":"7076883","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222973$7BF68387-48A5-401D-8F45-BF1F5BC548E7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f2e441e92fec06decae6ca757195c3c99a8473ed","datavalue":{"value":"ACTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$98842BDD-7E1E-4CC2-8408-3BD66AF8A60C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$06FBAEB1-AF44-4FAA-9D1F-7E911DA18C20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ebc2425e6015d5e2a26c14a2922e6263c0cbbd1","datavalue":{"value":"counterexample","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$FD0EF808-C506-4FE7-87FA-82FF0FE43EE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"940cb896d2a66fbb3a26f32752f8329203e8a303","datavalue":{"value":"deadlock","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$44225EFE-1B92-4CED-9AFD-773B203ADD42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf17229bc759b8968385466ece553a4bf034ef18","datavalue":{"value":"ECTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$8BFCEACB-3437-40AD-B960-7EBA0567E99F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$68D441C0-BFF4-42B1-9021-D096A3E529F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3336b0518162d61ed57d02a0de4e9d8d061f3981","datavalue":{"value":"witness","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222973$88F07F1C-1303-40B4-A902-DD826253E95E","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":"Q5222973$3736B06E-AF01-444E-A012-19CB6DBD5C74","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d2d31c62779e97702cb9d6096699da453944d391","datavalue":{"value":"https://doi.org/10.29007/2s1q","type":"string"},"datatype":"url"},"type":"statement","id":"Q5222973$A31B8E2F-BABA-4BDA-BD3B-9EDE211CE24F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9f246e1846241fc12e758c0ed3cd39c907d8b986","datavalue":{"value":"W2907427247","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222973$71C9383A-DB91-4C76-8E68-5BFD069F8771","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"41354c51d17798db5f633beb127386fa5f5ddb3a","datavalue":{"value":"10.29007/2S1Q","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222973$AD077DB1-2134-4B32-A27E-69781DEB523D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ad56d5cf5a0914eae3e1991359f1a1939c792e8","datavalue":{"value":{"entity-type":"item","numeric-id":5898914,"id":"Q5898914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4392fd4d8c2aea6844b96af55582625c2b29885f","datavalue":{"value":{"amount":"+0.9027178","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":"Q5222973$7C4A23BA-5E1B-42D5-B69C-54E9DD0133BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"974e0efd42fb163a438b8cd86c8ca828ce24edca","datavalue":{"value":{"entity-type":"item","numeric-id":2820781,"id":"Q2820781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d498bd3d776923e6c3c6df17e885dafd7c309a8","datavalue":{"value":{"amount":"+0.9022069","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":"Q5222973$80F4075C-C2C1-425C-9E39-C643F62263AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8c0a77f0232f67455c50d919d9a6fd0dceb2474","datavalue":{"value":{"entity-type":"item","numeric-id":5492979,"id":"Q5492979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"968e3f50095baab3dd93a8d04614d8596ee10a71","datavalue":{"value":{"amount":"+0.8992781","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":"Q5222973$9E696AC2-CA50-4520-A72B-A5E366640E6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6163a7aa78d81cf3b8065a62f631a6a5857595d0","datavalue":{"value":{"entity-type":"item","numeric-id":2754108,"id":"Q2754108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6e2f7b41bd5e6841456be17f40c855344057f0d","datavalue":{"value":{"amount":"+0.89079213","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":"Q5222973$F60E5B1C-FF84-4D7A-BFC0-380DB896F93C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7143ee151dba9462ec01595aed23567cde2f9b00","datavalue":{"value":{"entity-type":"item","numeric-id":5946344,"id":"Q5946344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"638813e7bab57a6ba93a8aa838834cd7912ac8c2","datavalue":{"value":{"amount":"+0.8877591","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":"Q5222973$AB6D5F83-576A-4BC9-B38E-99A6CC485B3D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5222973","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5222973"}}}}}