{"entities":{"Q5137900":{"pageid":7167471,"ns":120,"title":"Item:Q5137900","lastrevid":53882078,"modified":"2026-01-25T21:14:11Z","type":"item","id":"Q5137900","labels":{"en":{"language":"en","value":"Automatic verification for a class of distributed systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7281369"}},"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":"Q5137900$802B64DF-92EB-4EAF-A525-DFDF77374BF4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fd618a74d5c5b9e604a343e6322fb3b86dfe645f","datavalue":{"value":{"text":"Automatic verification for a class of distributed systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5137900$240189C9-DD74-462D-904A-CAA61B8C76FB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0ebd051e8c98f80ba4aefdf3f17fa2e1713d9b58","datavalue":{"value":"1448.68347","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5137900$8F8BAE15-1707-427F-B8E7-3867D77FCC67","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bb3c2ce650159601c8fca57a26a073792f1e6075","datavalue":{"value":"10.1007/PL00008915","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5137900$F3BBA9CE-5C90-49AE-9A3B-933101095052","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"144826b3df65da96c2e72eeb31ed1c271fa09bca","datavalue":{"value":{"entity-type":"item","numeric-id":1606534,"id":"Q1606534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$81561F5B-D212-4150-87A4-AB6FFF19674C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"df81383dd009ffaf5bdda4036e97feb3ff1168c6","datavalue":{"value":{"entity-type":"item","numeric-id":5137899,"id":"Q5137899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$BF73814A-00A7-4AD3-9612-D5E016E57F9F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"57115b4722082b3277b4db3ad0412a8293b7033b","datavalue":{"value":{"entity-type":"item","numeric-id":251292,"id":"Q251292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$E422B1CB-FE16-4D66-93F4-FF1C329DBAE3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"264ccd2874de70b65c9e8226185d78b9e2bc5a3b","datavalue":{"value":{"time":"+2020-12-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5137900$2E816248-8061-4A02-B807-259791BFAA6F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5137900$06701D3C-F2B5-4B5B-AEF4-A61B07613D7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5137900$555EFB16-3A91-463E-A7ED-FFB5A90B8C4E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"77bcb2c5c2dda7aee37f7e099542483131f8b5c9","datavalue":{"value":"7281369","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5137900$1F0DCAFD-C5DE-487B-8597-CC5AA8B9CFE6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e3ba7951b4903ad74bc8156ee379fa7f0472a6f","datavalue":{"value":"computer-aided verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5137900$44E2C84E-45F8-473C-AAA7-DBA510785DB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f82d9744537c8929843a9f698e900cd31ff81587","datavalue":{"value":"distributed systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5137900$EC7848E9-7230-4CF5-8828-698BA006B469","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ee25712a8d0e0d115e7cae6c46a5b59478b1622","datavalue":{"value":"state-transition systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5137900$38D0C985-32B0-44C7-98A8-3A7A958E8FD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8f46d1dd2f6c2dc9a9950c89b43a392741a7374","datavalue":{"value":"state-space reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5137900$934DD21B-7141-4145-9C9D-21C6BB9C7787","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"17cfe6afe68a54e81dc559ef2cd5a702765207b0","datavalue":{"value":{"entity-type":"item","numeric-id":25375,"id":"Q25375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$0A2F524C-E846-4EED-9BF7-2EC58E641CDB","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":"Q5137900$7EBC4971-14FF-4A9D-B178-978262EADE4A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"11ce10f2c105db58ec72d58d5665464175b07498","datavalue":{"value":{"entity-type":"item","numeric-id":921983,"id":"Q921983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$A029C5B1-7A1C-4762-A3EC-16F9A5A91042","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"090e4b104dd3f76f7e7cbd674cb41b2227a87ff1","datavalue":{"value":{"entity-type":"item","numeric-id":4692502,"id":"Q4692502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$8691FC4B-D5E1-4488-943B-6974A478AFBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47725b472606f4bada0befded8523598e0fad82a","datavalue":{"value":{"entity-type":"item","numeric-id":4302808,"id":"Q4302808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$89028554-D1A0-444E-8C88-CE5FF3E0FE69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0c7a4ff4d2625058b1a33aff6d79b66586396dd","datavalue":{"value":{"entity-type":"item","numeric-id":3769974,"id":"Q3769974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$E5447F44-370E-448B-B573-90C333B07514","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81b396b8939261a44fc48ea716bd927646197e09","datavalue":{"value":{"entity-type":"item","numeric-id":4302739,"id":"Q4302739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$739E1600-7CEC-4C5D-A3D7-CD3B252C0326","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"796364eeefb9789a01eab3a144d0337d6c23ee01","datavalue":{"value":{"entity-type":"item","numeric-id":1219675,"id":"Q1219675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$6C68831E-7BEE-4915-8E7A-DAEFC048B7EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68d7877f5c06b692012bb89ac63c690d31fa44f3","datavalue":{"value":{"entity-type":"item","numeric-id":3942371,"id":"Q3942371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$D81C6E4D-9F76-4F6B-9E79-7DC284F8AD71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40b5467bac8c2b14c65957d9305470ea5fcf1d67","datavalue":{"value":{"entity-type":"item","numeric-id":3911403,"id":"Q3911403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$DCE4F006-6E69-4995-A6E7-4182BCD33AFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1af915488af489df7f09b16bdb60f05e12a8b839","datavalue":{"value":{"entity-type":"item","numeric-id":1273576,"id":"Q1273576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5137900$A6358A5E-05D8-412E-A94F-15741CEA925F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e8b584b0cfe1c54b3c766993597b000fdb2f573","datavalue":{"value":{"entity-type":"item","numeric-id":4302808,"id":"Q4302808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0bc8461f3e4fd3f62515e89e920568044848e314","datavalue":{"value":{"amount":"+0.8035064339637756","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":"Q5137900$0609EC37-06CF-47F2-B994-B354918FE4A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21094922331cdcb7af8df158c52c67afe2d7acb8","datavalue":{"value":{"entity-type":"item","numeric-id":960505,"id":"Q960505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b56f1d7af96a2ca6431e6ccb3b350677c1ecbb3","datavalue":{"value":{"amount":"+0.7743956446647644","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":"Q5137900$05B1E980-BB7E-4C8C-9B0C-6AD3DB30F0E5","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":"c8d321faf271e976c792e4302dbcdb07cf5ff09e","datavalue":{"value":{"amount":"+0.7595211863517761","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":"Q5137900$67412416-D53A-40B0-BCA3-2E744BEBF770","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4f882e8c8c3f3b35fb5d6d6ebc7b6d3533c1972","datavalue":{"value":{"entity-type":"item","numeric-id":5505593,"id":"Q5505593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88dbc340481409cc21a2ad584f1d933f6ac31ab4","datavalue":{"value":{"amount":"+0.7563652396202087","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":"Q5137900$03053621-EBD5-4C2D-BAF9-B58E7F0803C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a94e17fc81ea7a9f45597b0cf471b6cf4d09c5cf","datavalue":{"value":{"entity-type":"item","numeric-id":4517043,"id":"Q4517043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ebee9d44af2575848baebe010ff58ab716e17255","datavalue":{"value":{"amount":"+0.7559457421302795","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":"Q5137900$50975B6A-F97B-41E5-A940-1C1281346647","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5137900","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5137900"}}}}}