{"entities":{"Q5015366":{"pageid":7044943,"ns":120,"title":"Item:Q5015366","lastrevid":58391469,"modified":"2026-04-05T00:35:40Z","type":"item","id":"Q5015366","labels":{"en":{"language":"en","value":"Efficient CTL verification via Horn constraints solving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7440189"}},"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":"Q5015366$0D7030CA-B3B7-4D49-9377-AA2E14698E20","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aa76d6dab28964ec2395d41eb4f1a91e916af3a1","datavalue":{"value":"1482.68134","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5015366$D38124E2-3CEE-4A83-A44F-19A13B632AE9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e454c70daebfcff7439a5cb57be0474ae652d8d0","datavalue":{"value":{"entity-type":"item","numeric-id":5015365,"id":"Q5015365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$3F111ECE-A384-457E-B9D1-D3A5702A7E4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"33f09e7b1eefa8c699a9d529da40fe033eb88541","datavalue":{"value":{"entity-type":"item","numeric-id":604393,"id":"Q604393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$DE1ACC10-2D43-48DA-8253-54DABC9F8E62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb5194b074431f4ab5210cd57ca7a7f1a1e79525","datavalue":{"value":{"entity-type":"item","numeric-id":948221,"id":"Q948221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$41A9EEEB-6D4C-4246-B112-20267B5D1FEB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"86e5bd0c18298fa85258b8271e23e3cb02a76cb7","datavalue":{"value":{"time":"+2021-12-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5015366$A09D6990-FDC2-47E1-BFD5-73864936CB45","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ad694978e019d3d366a0a2dec24d0aaa1068fd88","datavalue":{"value":"https://arxiv.org/abs/1607.04456","type":"string"},"datatype":"url"},"type":"statement","id":"Q5015366$565EE7E2-907F-44A0-9AF8-B7EE554D0D50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"daa50d5efbb885376a999c314a3fa88bd659ec52","datavalue":{"value":"http://eptcs.web.cse.unsw.edu.au/paper.cgi?HCVS2016.1","type":"string"},"datatype":"url"},"type":"statement","id":"Q5015366$D194F212-0B8D-421E-B659-A55CB0F24BAA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5015366$43A31C1E-DE23-44C5-B5AB-1701E4450B22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5015366$E285D07E-0774-4CA2-8EAD-2AC495E3F235","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"84a29c8f95563b6bcc942af2d69f4647ba794269","datavalue":{"value":"7440189","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5015366$0EC229C2-2424-4A5A-A963-F460DBC63387","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"49c5c39569fd0ed2872b7f9aefbae8dce402c98d","datavalue":{"value":{"entity-type":"item","numeric-id":21453,"id":"Q21453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$FD0D2DF3-04D6-450F-B3EE-D9D97D4DAAB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"341f73d8a5da3e56821659d4564aba270c8998c9","datavalue":{"value":{"entity-type":"item","numeric-id":53241,"id":"Q53241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$D957161A-33DB-400F-AD9B-B412AF9BD777","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1cb5c7412a95b8ff7f1ba4b73ca4c2023bf710a7","datavalue":{"value":{"entity-type":"item","numeric-id":21916,"id":"Q21916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$570AE4CA-324A-424A-869D-E8BF3402814D","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":"Q5015366$F838614B-0B8D-4873-A1FA-67E19E8329F0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"92fad865b077c2075f9e4a91ae650f98b63640c7","datavalue":{"value":{"entity-type":"item","numeric-id":3066089,"id":"Q3066089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$0D27AC41-4F2F-4979-A6AE-C28DE15AE19E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e5a7ec72f75de016381faf5e7bc0d67c18c7bcf","datavalue":{"value":{"entity-type":"item","numeric-id":5716758,"id":"Q5716758"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$9F6534BE-6795-451D-ACC4-7CE6D5317E11","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":"Q5015366$AE79F020-5A28-4A03-B577-376D3A4708B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"813bdce5005ea10f419962c6f94bdfc579587f49","datavalue":{"value":{"entity-type":"item","numeric-id":5429308,"id":"Q5429308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$49E1C943-D50F-4401-ABB5-BFB0EDDCC9DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6b20e36d097e4c5f2bb696f11d336fe5f6935f7","datavalue":{"value":{"entity-type":"item","numeric-id":4037084,"id":"Q4037084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$52486855-8AB4-400F-B990-596D8461FDCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1533546590c4a6b9a18b81fbbdbc821fd0f061be","datavalue":{"value":{"entity-type":"item","numeric-id":4640287,"id":"Q4640287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$96158AE8-47D4-4011-B2B4-007399FE7A07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5123548713629a223f9b5752ccd82f5449896b67","datavalue":{"value":{"entity-type":"item","numeric-id":2441713,"id":"Q2441713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$523F2B13-D297-4E1D-AD28-BE49360002DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f8c68f6ccbf13c46f9f52bbeb1df847a2fc02ca","datavalue":{"value":{"entity-type":"item","numeric-id":2901199,"id":"Q2901199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$341D3DF1-A9F1-447A-B129-22CBAB7938DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9005444265be022947046af02bafab842817cb2","datavalue":{"value":{"entity-type":"item","numeric-id":3189834,"id":"Q3189834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$C1363A22-D11F-4194-9C91-04B99176445C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7487e8571cba3063ef9a305ba5dd106faf1de1b","datavalue":{"value":{"entity-type":"item","numeric-id":1770366,"id":"Q1770366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$878F59B6-2C45-4352-AA5E-6FD24F7C1538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d0b3d39649082ff6de9169c6e51eb8e1d8d7a0b","datavalue":{"value":{"entity-type":"item","numeric-id":5385339,"id":"Q5385339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$A93ABEC7-D25C-4126-912C-838633266D05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4968b8cabc6e7e2146fbbb19353be5139e1037e5","datavalue":{"value":{"entity-type":"item","numeric-id":4002642,"id":"Q4002642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$D67997D2-4FE1-4D64-9C1F-7E5732849DE4","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":"Q5015366$9771DB07-2DFD-40C6-A4A7-56264F59E31E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62bf56316f400add0d0fd24e4ac8769d1d269f45","datavalue":{"value":{"entity-type":"item","numeric-id":3146278,"id":"Q3146278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$2625FBF6-6284-4909-84DD-4F98FB50F751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5410069e8abd75acf0c4dc99bb1a84758ddd17bf","datavalue":{"value":{"entity-type":"item","numeric-id":4187287,"id":"Q4187287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$2A0E91C3-DC96-45A3-979B-2142B02E32A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ed81dbbd1f03b6b81214d2ca7a802d60826d3f3","datavalue":{"value":{"entity-type":"item","numeric-id":3090847,"id":"Q3090847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$72A2ACA7-31A1-4CD2-A1FC-7577A6F67D3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"265238326dd3ecdbb898da1797f450d75dec4237","datavalue":{"value":{"entity-type":"item","numeric-id":2894269,"id":"Q2894269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$6DB67DD2-E18F-4659-A3A5-951243901A2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65ba6ee4184d1e83b23af04ea3e34386770ce9f4","datavalue":{"value":{"entity-type":"item","numeric-id":4472439,"id":"Q4472439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$60A6D733-E951-412C-9B25-4421AE9CAC7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a032d33673d5ba9c1e698848960782495104c1b","datavalue":{"value":{"entity-type":"item","numeric-id":1854405,"id":"Q1854405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5015366$A2F6A7AB-FB15-44C0-B391-BED788DAD0F1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3c9dca3a78a770850868382fd9a56590720a9de","datavalue":{"value":{"entity-type":"item","numeric-id":1702907,"id":"Q1702907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28ad0eb1d89a99a143b925052229723a9a2e619f","datavalue":{"value":{"amount":"+0.7712222337722778","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":"Q5015366$A7CC4B91-9A72-4475-ADB1-700B9A417CFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63018600324a71859f0d043848bacee9a1ae2407","datavalue":{"value":{"entity-type":"item","numeric-id":5930944,"id":"Q5930944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6a0accd7d67c4ccf5011eaf6db207f161bc7012","datavalue":{"value":{"amount":"+0.7614457607269287","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":"Q5015366$62260B54-3187-459C-9D86-497AC495ECCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94845cb0192c44f2f405da435c6139e86c20e67c","datavalue":{"value":{"entity-type":"item","numeric-id":3719811,"id":"Q3719811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a22a4dc5e1622536bd158893c9400bd0a208644","datavalue":{"value":{"amount":"+0.7614456415176392","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":"Q5015366$73E042E5-A8B7-4CAA-AB3D-62C16BBBDC37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5a5bb51e3095387c40d880ae273a0fce71d2c1c","datavalue":{"value":{"entity-type":"item","numeric-id":2947164,"id":"Q2947164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3bb531f19c3cb6f9339f25c7ef9faa1a7af2846d","datavalue":{"value":{"amount":"+0.7559259533882141","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":"Q5015366$812EF25F-0599-4F48-AE7E-BA3382926842","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"471e675447a5a733f8fe932bd3d6563dd29b78d3","datavalue":{"value":{"entity-type":"item","numeric-id":4640287,"id":"Q4640287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f89215c0782c52ec6a790f42baf87027b9b9ddf","datavalue":{"value":{"amount":"+0.7538191676139832","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":"Q5015366$9D41B45C-99A5-4D72-85C2-1A96E380CC13","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5015366","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5015366"}}}}}