{"entities":{"Q2026564":{"pageid":2037306,"ns":120,"title":"Item:Q2026564","lastrevid":72439476,"modified":"2026-04-14T04:55:20Z","type":"item","id":"Q2026564","labels":{"en":{"language":"en","value":"PPTL\\_SPIN: a SPIN based model checker for propositional projection temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7349927"}},"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":"Q2026564$AF5DAC17-E5BD-44F1-893C-9E21959406B4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c3f53cc3fd8024c81562bb5e016e23178f28ff02","datavalue":{"value":{"text":"PPTL\\_SPIN: a SPIN based model checker for propositional projection temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2026564$906D3C08-737E-496F-A032-BD2E2F531768","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"60ea6edff211c743478668306f31f9d512fb14f9","datavalue":{"value":"1461.68124","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$7F226A47-92D5-491F-AF1F-9FC13BF97178","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8fd99b8666c72cbabbf63736300b18c8a5123a4d","datavalue":{"value":"10.1007/978-3-319-31220-0_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$F61EFF4D-8679-48F5-84E4-535B89D773A2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2026564$C2E0FA12-9BDA-4B4B-BDC9-7B2D5EB13150","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"211031a52806337129a1eef00df007a6622a5387","datavalue":{"value":{"time":"+2021-05-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2026564$E9FABE09-5713-49C7-8730-41959D80BCD0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$D52F0223-B316-4E35-AF3A-7B49589B6612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$26B57A86-BD83-4170-93E4-D5C1518ED537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c270fb88a62fde738bd530246c5ba57a005a4efd","datavalue":{"value":"03D05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$A05B5483-0DAB-44F9-9683-856D770FC73B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$E92FE81D-D0CB-4036-8428-5A8671156F46","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"728a1cb4283b565a8f56ac707c70d4d53b87dfef","datavalue":{"value":"7349927","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$F5DCE634-F068-42E4-A676-E50EDD19BD3B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7f6c80b0dfc69f07b6732579007eac69eb2f8c4","datavalue":{"value":"propositional projection temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2026564$F0D20F36-CF3F-4E3E-9A3C-262A9A800587","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3db880c44e3892417a5400283a3d37c5f9553d1","datavalue":{"value":"B\u00fcchi automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q2026564$61A6E7E9-4EA0-422B-B8F2-626AA0F238A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2026564$5BE03A1B-CAA5-4FE8-A552-C30D290A3651","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"772c4ee50d131f1a35ff4b31da11ffcdcf02c815","datavalue":{"value":"SPIN","type":"string"},"datatype":"string"},"type":"statement","id":"Q2026564$4435E03D-D0C1-488B-92A9-256C145BEDC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2026564$94ED5456-B380-43E2-8970-0887BDC8217B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"53a4a9b6c38d395d5b2eb80cedc3eefcbf3e9947","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2026564$2D853D34-037A-4440-B94E-710512FE8DF8","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":"Q2026564$49AC9EDB-9F83-4E21-8A51-550F199A3067","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"41846cfefd0bf47de7a06c4dbcebad69a1c08b3b","datavalue":{"value":"https://doi.org/10.1007/978-3-319-31220-0_14","type":"string"},"datatype":"url"},"type":"statement","id":"Q2026564$D494E8BD-D001-46F2-BD41-036B08454242","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"73d0be0026837a47ace968897423e52751c6148d","datavalue":{"value":"W2460979775","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2026564$2DD0507C-6BDC-46DA-987E-F9D690D964E9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f6b7498f5920637787f322928d176bdbab0ec91","datavalue":{"value":{"entity-type":"item","numeric-id":3461297,"id":"Q3461297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6802a68445d036aacd38dd6405c04eaad38fdb39","datavalue":{"value":{"amount":"+0.8503952622413635","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":"Q2026564$2E442FCA-6A1C-408E-99CD-61EB22B1FD7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9bc0d0a982a32d3b01e7797b4f0d8f4a290eca8","datavalue":{"value":{"entity-type":"item","numeric-id":4925273,"id":"Q4925273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c5defe7f21f8ccfac7b6572faa39cfd4bed0d817","datavalue":{"value":{"amount":"+0.8493558764457703","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":"Q2026564$967E426F-5BA7-462E-A7DC-9AC8CA20E25B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a53ddec00cff2a34b2596ffc0f8f38c60adad626","datavalue":{"value":{"entity-type":"item","numeric-id":896152,"id":"Q896152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbbd5de04ac5fb46672dc5119020b3b20abbcf80","datavalue":{"value":{"amount":"+0.8353303670883179","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":"Q2026564$216CE72C-50E0-4397-9F06-D42DBF0D712E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba5f2906d9500e896f65ea45b170c431d3117efd","datavalue":{"value":{"entity-type":"item","numeric-id":2824415,"id":"Q2824415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17c0b5cc512e755ef8aec8fe4c4b6593c4f3f069","datavalue":{"value":{"amount":"+0.8007280826568604","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":"Q2026564$C4AA8AF0-FA2F-424D-B6F3-70C0DE6AF51C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b86d0541e0fa03c640aace3d612ac080587bd37","datavalue":{"value":{"entity-type":"item","numeric-id":2300069,"id":"Q2300069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef223926ec56b63df17510c70e2d0e74754f8bec","datavalue":{"value":{"amount":"+0.7933754920959473","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":"Q2026564$DE7B2F14-BD58-43DC-A2CB-9AE38B24CE45","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"PPTL\\ SPIN: a SPIN based model checker for propositional projection temporal logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/PPTL%5C_SPIN:_a_SPIN_based_model_checker_for_propositional_projection_temporal_logic"}}}}}