{"entities":{"Q5009450":{"pageid":7039027,"ns":120,"title":"Item:Q5009450","lastrevid":91274621,"modified":"2026-06-04T22:44:03Z","type":"item","id":"Q5009450","labels":{"en":{"language":"en","value":"The satisfiability problem for unbounded fragments of probabilistic CTL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7378576"}},"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":"Q5009450$52AE5E03-8384-489F-B588-FC2DA0BC8495","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8e4018f669876a5819cf16362b14fc078dbd59d6","datavalue":{"value":{"entity-type":"item","numeric-id":690503,"id":"Q690503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$9B675A90-DB97-4462-9D79-43E4E7AEEA30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a3916bf04a7d3b824dfb3a91afc882d2b96beb34","datavalue":{"value":{"entity-type":"item","numeric-id":5009449,"id":"Q5009449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$09494A3B-B39C-4450-A5F1-52710D6C449C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6f25f924676185979ab6f246b476dde833797f44","datavalue":{"value":{"time":"+2021-08-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":"Q5009450$68F2192C-C150-405E-A777-B68A91623BE5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"40381ca96ab9e764bcf947e9b26d51d5343278cc","datavalue":{"value":"https://arxiv.org/abs/1806.11418","type":"string"},"datatype":"url"},"type":"statement","id":"Q5009450$AEFD1C72-EF10-41D1-A852-CC7BEBB1989A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5009450$FB0C4CB7-B44A-4904-BEBC-4E72BBC8AE53","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6a5e49be3b52df8e75b8a3e2178f310eab42bbd0","datavalue":{"value":"7378576","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5009450$5FD606FA-BDD9-4DD6-BC9D-E865F116A250","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5009450$04564934-8E7E-4114-8A5F-935B42C1993D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6f7b890de0bb5e9d45d15d280bf18eeaefac20c","datavalue":{"value":"probabilistic verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5009450$CE06CEBD-6C9A-4F94-8ABA-01D209992D96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e5d1640a9a10bde209aad98fb59b1050a4cb674","datavalue":{"value":"probabilistic computation tree logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5009450$6D6FC99F-B401-42F6-94DC-7B495D1CB8BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q5009450$7B92D1A6-A03A-4F5F-81E3-2D0A156D8152","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":"Q5009450$E5BB7A0B-C977-4765-9F75-567432421182","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b52479ce1aed3445cf12b4ee9e791997db4f08cf","datavalue":{"value":{"entity-type":"item","numeric-id":4673428,"id":"Q4673428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$02B77FDF-5894-4E71-AA61-5862DE411466","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":"Q5009450$2838F2B2-A4D8-493F-AA05-C9016C79E585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0814ccfe28635eee2940f324c80610763cfcfe12","datavalue":{"value":{"entity-type":"item","numeric-id":4649540,"id":"Q4649540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$933C8D99-FF3D-46A9-80E4-C62B1938840D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"176492351b6803d6dd45cb238a6cda64a727f5fe","datavalue":{"value":{"entity-type":"item","numeric-id":3519498,"id":"Q3519498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$90AA29A7-E4A8-4F55-8F23-ECE543CC93CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d65cc8f2e5ea23c3bd01560d132b8a831f35fc62","datavalue":{"value":{"entity-type":"item","numeric-id":5710670,"id":"Q5710670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$E7D2D1FD-C4EE-4EF9-8448-721AE631A3B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e55b625be6ffdd7aadd5c06bddc56ae1684a5a3","datavalue":{"value":{"entity-type":"item","numeric-id":4635861,"id":"Q4635861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$5EBACAEA-682A-47C7-8074-E57EAD89468E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c71ee253892b177799592f03938a61eb6c7732cc","datavalue":{"value":{"entity-type":"item","numeric-id":4369884,"id":"Q4369884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$C70B8E68-ABEC-4210-92BB-0856C757995A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4ad3f590870ee5c4bb6817717a648be99f36b59","datavalue":{"value":{"entity-type":"item","numeric-id":2388726,"id":"Q2388726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$00112438-BC0B-48E9-8FEF-834B2E36C70D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a9d1825e985bd9d3ac22966e44befbddbae3977","datavalue":{"value":{"entity-type":"item","numeric-id":5310649,"id":"Q5310649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$8787EF81-55A2-48D2-8017-5FE1E78EA059","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b1af63d4fb1b182e57889faf02ebb0ec9fbb312","datavalue":{"value":{"entity-type":"item","numeric-id":5710687,"id":"Q5710687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$760D443E-0615-4379-9CEE-721C5ECE7C29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47c57a1bc98a9d819c8c4b25347f0c45d96256b1","datavalue":{"value":{"entity-type":"item","numeric-id":1258296,"id":"Q1258296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$EEBF157B-23CB-450C-8859-9D5A5E61FAD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e53d9e53c3c574e8c7675f6ec5036e8ca0ad199b","datavalue":{"value":{"entity-type":"item","numeric-id":1343864,"id":"Q1343864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$E36FC90B-47AC-4D4F-9655-307158F53E46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a94ce82facff0f2e4f1d67b6e302024de8cbe6f0","datavalue":{"value":{"entity-type":"item","numeric-id":4722046,"id":"Q4722046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$215566EC-33A3-4D46-AFA4-63E24E07A5B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a26a1af667e232ab14af2dc3552831d3e45f382","datavalue":{"value":{"entity-type":"item","numeric-id":2368950,"id":"Q2368950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$F942B99A-AE48-40B7-A926-6137301EA3A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54f1ad840706c682b0fedd77190bd24d7fda2981","datavalue":{"value":{"entity-type":"item","numeric-id":1117213,"id":"Q1117213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$C5C9C2BC-C317-4076-AFE4-45EA4438F252","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0840a97ff84a8bbb1684d812172c86ef7c121a6d","datavalue":{"value":{"entity-type":"item","numeric-id":5897798,"id":"Q5897798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$158205FC-8B3E-490E-A2E7-8FB95B4FC0A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39e952539371341c17224ee9b3086414796d0340","datavalue":{"value":{"entity-type":"item","numeric-id":1781404,"id":"Q1781404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$6FA94028-BBC3-41B4-BE87-02B623AD99F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"576c170a64464a75151001e4ed4c1d0949344c42","datavalue":{"value":{"entity-type":"item","numeric-id":3337452,"id":"Q3337452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$18272973-7E27-4B39-A558-D9DCA3750A02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18642a838491c188ef18e183a8a792128a59fc0c","datavalue":{"value":{"entity-type":"item","numeric-id":4216130,"id":"Q4216130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5009450$51B876CC-8A54-41B9-8F5B-0581875B3EB1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"93efa6f2b92a52e7b30b098b249bf68356eba99b","datavalue":{"value":"10.4230/LIPICS.CONCUR.2018.32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5009450$1E98AF84-7C66-4FE9-9F44-AAC295E8C22C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e41f1a17c84a20e42684c096b88b1ee9405cbc0f","datavalue":{"value":{"entity-type":"item","numeric-id":4635861,"id":"Q4635861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11e5bb73874f1e92280239e7862e06e8dddd9e38","datavalue":{"value":{"amount":"+0.889532744884491","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":"Q5009450$E2F9E300-398B-4F1C-9AFD-C13F28A76EED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"594223055631fa30a4b664f19e8d98f03aee1591","datavalue":{"value":{"entity-type":"item","numeric-id":4649540,"id":"Q4649540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"759bfb15faca7517bc43d245bf9dfead2d8304ce","datavalue":{"value":{"amount":"+0.8084869980812073","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":"Q5009450$D0BAEE5C-49F0-4EBD-91E0-2AE3DC11C8C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab234acaf5c68faf52640a6c31bd122fdc22d598","datavalue":{"value":{"entity-type":"item","numeric-id":3646173,"id":"Q3646173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdf820ffc47f30d9cd85b2d0bbc1fb77335def39","datavalue":{"value":{"amount":"+0.8070241808891296","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":"Q5009450$18794ABC-0CBA-4335-BCED-FC5D7B6F6AD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4dcc74f5016755b382c73656c29a163b4f17aa71","datavalue":{"value":{"entity-type":"item","numeric-id":4982095,"id":"Q4982095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18a80be954d5bc0323f8f496aa168f8f3fd9cb85","datavalue":{"value":{"amount":"+0.8059815168380737","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":"Q5009450$D1D35F95-C346-4C5E-AAE3-8FBD46D0A755","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72bdbbfa4f2c18ac7eac3b20693c4e3593ec35e1","datavalue":{"value":{"entity-type":"item","numeric-id":4914007,"id":"Q4914007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a972bf75bbdbfc46f9c2a5d177c9ae756ef6cb7","datavalue":{"value":{"amount":"+0.7971628308296204","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":"Q5009450$A2DFDF0B-C61F-4165-98C4-38E22A8DD644","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The satisfiability problem for unbounded fragments of probabilistic CTL","badges":[]}}}}}