{"entities":{"Q1856161":{"pageid":1866903,"ns":120,"title":"Item:Q1856161","lastrevid":69121656,"modified":"2026-04-13T04:55:20Z","type":"item","id":"Q1856161","labels":{"en":{"language":"en","value":"Practical CTL* model checking: Should SPIN be extended?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1862275"}},"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":"Q1856161$6E9F8CBF-79DD-4B34-93CF-81EC13E4C5FF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3a4db74f3c80baf14c591b984f1656fc33217acd","datavalue":{"value":{"text":"Practical CTL* model checking: Should SPIN be extended?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1856161$F8995852-73C3-4AA6-A71B-950A38230077","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"02fdba1e4031102fe8c731547102219ef6e74d77","datavalue":{"value":"1059.68591","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856161$3E4D36E1-0285-4B32-B73A-33A7A20251A6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"04935240de55a949343a0104f6137af940dc941e","datavalue":{"value":{"entity-type":"item","numeric-id":816188,"id":"Q816188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856161$0E828D9B-FF1A-4FC6-9BA7-4010FFE37CB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"33d000139a62fd77e59fd5eeddbef5ca99d4a3f4","datavalue":{"value":{"entity-type":"item","numeric-id":934705,"id":"Q934705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856161$1E75CFD2-5DD2-4FE8-B143-1C0348A21ED1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e1846ce75b2b308fd593b292d943abd351ca6751","datavalue":{"value":{"entity-type":"item","numeric-id":225063,"id":"Q225063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1856161$BC8B22E5-FCCA-4CA2-A0AE-4048FD16983A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"51fa866876a61ae2435740199de51e5bb1a31ee7","datavalue":{"value":{"time":"+2000-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1856161$5D1396B0-E48D-429C-9376-FF6B8B3B3CC6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856161$033ED5C1-D6B4-48B7-805D-171E47060332","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856161$85883160-A51B-4989-8A26-923591329644","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"787c2d90462be20e79497bfb12a1c896b5f6f16f","datavalue":{"value":"1862275","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856161$9449F321-68F5-4044-8472-E52018888131","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856161$B297A3E0-80F9-4B0D-88BF-E7CEF9A5EA6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3db880c44e3892417a5400283a3d37c5f9553d1","datavalue":{"value":"B\u00fcchi automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856161$E550BB69-5A38-440D-849D-5E16A44A1D34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"006d94939042b66d9a377878845627ba6e1a4e29","datavalue":{"value":"hesitant alternating automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856161$E33E8D46-AA23-4E66-8D01-CF88369CFAE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dc9a47c8de051a880f2e514b2df8fca32ac201f","datavalue":{"value":"games","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856161$6DDA9C91-83DA-474D-A81B-2EA3F4DCE956","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"772c4ee50d131f1a35ff4b31da11ffcdcf02c815","datavalue":{"value":"SPIN","type":"string"},"datatype":"string"},"type":"statement","id":"Q1856161$6C9D1841-58B2-485E-9347-6D51E34CDB3F","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":"Q1856161$9E9EC205-2CC4-4EB1-BA0F-3751F567E8F2","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":"Q1856161$7A4AE696-7948-4C06-8B7A-07534277C27F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"43d36ea1bc4ed0ab4de397b8cbb51aa2b8287c73","datavalue":{"value":"https://doi.org/10.1007/s100090050042","type":"string"},"datatype":"url"},"type":"statement","id":"Q1856161$1BD40DAB-8C57-4347-8615-A8976315FC4F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6ac00c11debb2eb587a0701b4467d7b7f93faa97","datavalue":{"value":"W1979424379","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856161$CA2A9224-13AE-47CC-9835-197FB5D4AB32","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"66041444e7b5cc964f53f2def2a4ef072e87687f","datavalue":{"value":"10.1007/S100090050042","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1856161$BEBF2688-8308-4687-8454-48EFF8872880","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca522f2f833db3826493b39383074bf163777bd9","datavalue":{"value":{"entity-type":"item","numeric-id":2848152,"id":"Q2848152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ab8bcce356935dc6fd797200a05c438323424f0","datavalue":{"value":{"amount":"+0.7830038070678711","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":"Q1856161$4D64DB73-0802-4B5A-9F4C-30E76E3F348D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84f5f09a1984d0a03a303ec39095aadc5588f747","datavalue":{"value":{"entity-type":"item","numeric-id":5703759,"id":"Q5703759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8e6aacbd13711139d0b6009fee52c49a01b0290","datavalue":{"value":{"amount":"+0.7776339054107666","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":"Q1856161$63AF30AD-B562-4DA4-B804-8DD534E4377C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"486d5c88d1a1e744d0ef79c863f6f0b287e1435c","datavalue":{"value":{"entity-type":"item","numeric-id":4531762,"id":"Q4531762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4759b108e6f0850f801f0074a13c01f91faf3316","datavalue":{"value":{"amount":"+0.7725003957748413","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":"Q1856161$F55B2620-F60D-4006-8D2F-2A73C31327C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9fbc54422c85d4d1580c3b18f9b4b9c82ba7497f","datavalue":{"value":{"entity-type":"item","numeric-id":4938419,"id":"Q4938419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"782e16a01d3bef7b5f1b7c93089f31321d9d17cd","datavalue":{"value":{"amount":"+0.7600870132446289","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":"Q1856161$259EA0E4-94BA-4EE9-938C-4E975047193B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75e2e1203d7e5b8db467a268311da63c0244b664","datavalue":{"value":{"entity-type":"item","numeric-id":402129,"id":"Q402129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"782e16a01d3bef7b5f1b7c93089f31321d9d17cd","datavalue":{"value":{"amount":"+0.7600870132446289","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":"Q1856161$9D644A1F-58B4-4477-891C-0FC05FC0F884","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Practical CTL* model checking: Should SPIN be extended?","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Practical_CTL*_model_checking:_Should_SPIN_be_extended%3F"}}}}}