{"entities":{"Q2851976":{"pageid":2862696,"ns":120,"title":"Item:Q2851976","lastrevid":51838490,"modified":"2026-01-20T07:17:22Z","type":"item","id":"Q2851976","labels":{"en":{"language":"en","value":"Using agent JPF to build models for other model checkers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6213598"}},"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":"Q2851976$C58080E9-43CD-4982-A1FA-60F68A78DA52","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b1d41ab45a4065b8dacafab2f855ea70f6bbd72f","datavalue":{"value":{"text":"Using Agent JPF to Build Models for Other Model Checkers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2851976$07CDB79A-44E6-4CDF-A0D0-85965919E617","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0da8023adce080253b3d65b73fa785217e878f08","datavalue":{"value":"1401.68192","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$A1D6AA4C-63C0-41DA-9815-7C99D3438E05","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b84c5215720012542356ff66f2d954d047bb19d6","datavalue":{"value":"10.1007/978-3-642-40624-9_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$41422558-7BDF-4ABB-819B-0ACE3307BEFD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$053D70DA-5714-4702-B506-91A0F9A95A3C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1145dc38b4d246480a51682f22dd7d8a161033fa","datavalue":{"value":{"time":"+2013-10-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":"Q2851976$FFDC0A94-49CA-476F-B53A-DF1DB0B68048","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$4CF8D0B2-794F-4C66-9C9F-45D9569388DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35c3f01235ccba091e1644bb05c86f53d45fd7f7","datavalue":{"value":"68N19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$0AA04AEB-B1E4-4BFC-B4D1-D4DA2B9F038F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"30d03bf839650c03e960334282e35ced22330952","datavalue":{"value":"6213598","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$DFB167A9-6A60-42D1-B4EA-2E11BE960837","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"531a52a4ab12ab6e2b5be84834036762ed677445","datavalue":{"value":{"entity-type":"item","numeric-id":13928,"id":"Q13928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$4DF69D78-A058-4137-9B19-B9C65DFE5E34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af5bf62d73c7ce629c0669b5ccd1badd6d3f9691","datavalue":{"value":{"entity-type":"item","numeric-id":21446,"id":"Q21446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$6C24E900-DB6E-4C7A-9599-B1DFC32B1158","rank":"normal"},{"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":"Q2851976$413CB592-7B9B-42A1-A1EF-07A56DA4943C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0e08ce1ac46e4dcfa9d24dbe5d8c871a26ae1956","datavalue":{"value":{"entity-type":"item","numeric-id":40213,"id":"Q40213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$DD1FED86-F737-4064-8A16-079F354195D8","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":"Q2851976$B55DC4AD-7605-4B3F-AEAD-9F1A1E522EA6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e61edb5fc131724f5c7a7303dca8c0f0cbc85c8d","datavalue":{"value":"https://doi.org/10.1007/978-3-642-40624-9_17","type":"string"},"datatype":"url"},"type":"statement","id":"Q2851976$A3DEB5CF-4F80-4340-97CA-31ABF6C6C33B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"913c5dc95d5c0dc7511c4acbd37b4f6a3c9f1d5b","datavalue":{"value":"W1503257619","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$E9FBD291-C566-4D66-A03A-4AB8797B01EF","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"568dd8fd1df93e7d45a780ab1036f85de4c82d80","datavalue":{"value":"Q98283461","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2851976$AEABCA99-368F-4069-8B81-990AE1E9B88E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ff7e731a225299809c7217b779a74b446dd9c768","datavalue":{"value":{"entity-type":"item","numeric-id":540691,"id":"Q540691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$B694BC82-E557-4DE6-B4EF-DC6CE9BF6637","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"081ff692cfa31ae371e8cdc5bc8cc37fc96a3d18","datavalue":{"value":{"entity-type":"item","numeric-id":6102168,"id":"Q6102168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$3C115650-0479-4329-88BA-62994F45F48E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9d1130ac45bd162bb19fc0ed5c7d75d89ada19a9","datavalue":{"value":{"entity-type":"item","numeric-id":6772985,"id":"Q6772985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2851976$36EF55CF-7FAA-4166-9373-783729295197","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c6914bfe57cc5668ec2c8fa0e5ae6940ff01b4f","datavalue":{"value":{"entity-type":"item","numeric-id":4612415,"id":"Q4612415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a8d2b191d62af58c78c66e9be534d7a1a4fd00f","datavalue":{"value":{"amount":"+0.9085461497306824","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":"Q2851976$8A7217B1-12D2-46CE-9B1A-3B0713EB9E66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"496e8c62b1ceff8dbec4b3b16f9be0febb6ca009","datavalue":{"value":{"entity-type":"item","numeric-id":3056328,"id":"Q3056328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61d36bc50b8d39df8edcf0e5ea036e266d344162","datavalue":{"value":{"amount":"+0.7371768951416016","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":"Q2851976$7D86C7A3-1ED2-4DCC-8951-5A7AFCC27909","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddab87631d4a081dbd128c7a792d799b2a6c7e03","datavalue":{"value":{"entity-type":"item","numeric-id":1856163,"id":"Q1856163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18ef77308b5ebde350e932e607b2ef3caba76f33","datavalue":{"value":{"amount":"+0.7192323207855225","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":"Q2851976$549D0000-4610-4D38-84F3-7FF80FA41518","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ad86a46220de377846c2d131ca6c44cfa8b51af","datavalue":{"value":{"entity-type":"item","numeric-id":5898020,"id":"Q5898020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f30085567fdf6271e7b3e2092198d480b41d4bf","datavalue":{"value":{"amount":"+0.6928853988647461","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":"Q2851976$EACA591E-7A14-48AA-888B-7527431C615C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"305601bd10e4543ee41f5a7c6bc2673dbabf52b6","datavalue":{"value":{"entity-type":"item","numeric-id":4209291,"id":"Q4209291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7388be271e9f9a2db5cf13f5e38c277d6d7caacd","datavalue":{"value":{"amount":"+0.6920862793922424","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":"Q2851976$B07FC623-7410-4007-85EE-47FB669FE7EE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2851976","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2851976"}}}}}