{"entities":{"Q678251":{"pageid":680100,"ns":120,"title":"Item:Q678251","lastrevid":63524733,"modified":"2026-04-11T13:45:04Z","type":"item","id":"Q678251","labels":{"en":{"language":"en","value":"Using the causal domain to specify and verify distributed programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1000549"}},"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":"Q678251$02A47371-077A-49C4-A469-5ECC1B75FEBB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"055a3a8d34d695798ed4291dbe1c3b77a9d8c3e2","datavalue":{"value":{"text":"Using the causal domain to specify and verify distributed programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q678251$580259CD-1423-4214-8D80-AB239A8D163E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b29c43d3eeb8c4f4e7331f0f7dc15bcc48761f0a","datavalue":{"value":"0878.68085","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q678251$8E70E159-E8BD-444E-A5DF-92F1FCA99BAE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f45f82d5e189cd4082ece2dd91de330307ec2b2","datavalue":{"value":{"entity-type":"item","numeric-id":287189,"id":"Q287189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q678251$603A5639-594B-4138-95B4-3FEE0CB81D82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"87693f4598d10df1c7840e8a89f743cde7382f7f","datavalue":{"value":{"entity-type":"item","numeric-id":678250,"id":"Q678250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q678251$26F2EF4B-ABD4-4FF3-8BDB-D44C3C38ABB6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q678251$317C08BE-653B-4811-B9D4-407FA240ED73","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d055fb3109bca705377a91671f6048909534fe40","datavalue":{"value":{"time":"+1997-09-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q678251$8FC35A8D-9F07-4084-BE88-D46522E9F938","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"83865eacfe6564dac493146bd7129b29de344c8c","datavalue":{"value":"A system for specification and proof of distributed programs is presented. The method is based directly on the partial order of local states (poset) and avoids the notions of time and simultaneity. Programs are specified by documenting the relationship between local states which are adjacent to each other in the poset. Program properties are defined by stating properties of the poset. Many program properties can be expressed succinctly and elegantly using this method because poset properties inherently account for varying processor execution speeds. The system utilizes a proof technique which uses induction on the complement of the causally precedes relation and is shown to be useful in proving poset properties. We demonstrate the system on three example algorithms: vector clocks, mutual exclusion, and direct dependency clocks.","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$92A319E1-B90E-4399-B72E-DEDBA82890C5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q678251$30BD878D-D041-440D-B98D-85ED0349BD9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q678251$84A81F6F-38DA-4A57-9435-38D0F736678C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c681881ffbdeb3a05ab838eb7759b8532e524ff4","datavalue":{"value":"1000549","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q678251$6C81D459-624A-4988-B7F5-28B112DD61BE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"126bc261b4ce15426bca501a6725c284417e2bf6","datavalue":{"value":"partial order","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$20357D4D-1260-4575-8039-C6A67FDC9CE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c40ddf808060ba42d097128ffb37e89bf3adfd06","datavalue":{"value":"causality","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$A59C4277-8638-4085-8E08-D4C2BD4866E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df040f138da0195d6bf7ee04b2cedfdeb81adbb9","datavalue":{"value":"program specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$4129A3A2-53E0-4AF7-9800-2DB74B421A06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df198e9539af8ee1221a27fc303d184b5cc81a2c","datavalue":{"value":"program proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$95E68356-D9EF-4455-B7E9-B4D49A4A3E58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4047d80d54126035960b906b0c02ba643492c81c","datavalue":{"value":"vector clocks","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$4DB5792D-8FCA-4BAD-8449-DFB79B4C7DD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"995b00cc7d69ee07cf24da51a3a5485ed2bb2d30","datavalue":{"value":"mutual exclusion","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$E2205165-57C3-4320-8431-67A77E2A7E9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b12ab8d7dab6795fa09dabf93d30c8e2005251ca","datavalue":{"value":"direct dependency clocks","type":"string"},"datatype":"string"},"type":"statement","id":"Q678251$EA4267CE-A61C-4C0A-9B6E-22A02FEB7D81","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":"Q678251$180C01D8-1F46-4C43-A9EE-A459C898D38E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2bb544d7619358fa4b8eaaf5c54d87f229340aed","datavalue":{"value":"https://doi.org/10.1007/s002360050102","type":"string"},"datatype":"url"},"type":"statement","id":"Q678251$7BA07B61-1DBC-403C-AF59-79750D6B12CA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b6193a295cc6a40b3608fb4a66d0206691f2c174","datavalue":{"value":"W1968857745","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q678251$1818768C-2F62-40D2-B264-30099D9410A0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bb2d2021ec01111069851e1d7cc0bf61f45a4f61","datavalue":{"value":"10.1007/S002360050102","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q678251$8D7D92DE-C099-4DD1-A4B3-66EDF92B1051","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b9e26ade5b17f925b40386334e9b06436a14a58","datavalue":{"value":{"entity-type":"item","numeric-id":1893537,"id":"Q1893537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42cdc67d4b4557578fa0784df9423be2cbf5fc5e","datavalue":{"value":{"amount":"+0.7709463238716125","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":"Q678251$7FB53C4A-4E35-4995-8406-189F70579BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4657f223a476d3721ee27cccbd9cb0e5c9544240","datavalue":{"value":{"entity-type":"item","numeric-id":1200917,"id":"Q1200917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"073dc27a13e64665f50e3d120a114aca8205e5ea","datavalue":{"value":{"amount":"+0.7475630640983582","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":"Q678251$BEB3427B-BCA1-4F55-BDC7-8DA645A6A882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3453d1b8e17d669a142e87f9a3136a8bbabdb1a7","datavalue":{"value":{"entity-type":"item","numeric-id":1193762,"id":"Q1193762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fefe72878b2bf938d86d87847ee4d358477bcaf1","datavalue":{"value":{"amount":"+0.7397326231002808","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":"Q678251$E1266951-1933-4C9F-9A49-07A3E182A5B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c231767e805dc68277b675ed1ccd29e9e10d1d98","datavalue":{"value":{"entity-type":"item","numeric-id":4733386,"id":"Q4733386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b59796cd846df36d161dff8b2fa1913b808bdc9","datavalue":{"value":{"amount":"+0.7387788891792297","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":"Q678251$88187E62-80C5-431B-84CD-7AE51D121EEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2e98bd4c932342579ceaa19841cf9af737500e1","datavalue":{"value":{"entity-type":"item","numeric-id":4038718,"id":"Q4038718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c840890586c0a652a9a8c5c3637fac75dff2d353","datavalue":{"value":{"amount":"+0.7378937005996704","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":"Q678251$3543C21F-7629-477E-AF55-F47A219C6C8A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using the causal domain to specify and verify distributed programs","badges":[]}}}}}