{"entities":{"Q1330425":{"pageid":1341175,"ns":120,"title":"Item:Q1330425","lastrevid":43036387,"modified":"2025-07-17T02:53:58Z","type":"item","id":"Q1330425","labels":{"en":{"language":"en","value":"A trace-based compositional proof theory for fault tolerant distributed systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 609565"}},"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":"Q1330425$94078FD9-3CBD-4860-A3C0-EF872E4443F1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3d03eadc15acd439aa9e848740377a0a86de322a","datavalue":{"value":{"text":"A trace-based compositional proof theory for fault tolerant distributed systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1330425$3E3F02F2-0F5B-43D3-B089-1CAA8742E04A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f5ebd007510db76e52842a59dc61eda3910583b4","datavalue":{"value":"0812.68094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$EDBD77FA-19F5-4D61-BEFA-8356328F2414","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"01f2399610615d7117ecaadf2e23e50836f64ffb","datavalue":{"value":"10.1016/0304-3975(94)90167-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$ADDA7A58-6F47-4E03-A58C-870F02EBBE8D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d0a634fd8c610a56db676a38c3ab90d5b223b43","datavalue":{"value":{"entity-type":"item","numeric-id":1330424,"id":"Q1330424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$8F6BCE27-7E73-43FD-9A1C-092FC51D8CF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"655b272f9711e4d9ee9172807da80e0536e6347a","datavalue":{"value":{"entity-type":"item","numeric-id":229991,"id":"Q229991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$B6A6DB46-9F27-4817-9E02-9C0FC3E8B5EB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$F9554461-5D75-4EBF-9F11-C3BDEB468D0B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"71edc96fcbd008bfd3061c3ff4af97a6b34cf242","datavalue":{"value":{"time":"+1994-07-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1330425$4978B88C-CD35-40F1-AFA7-71D33755B44D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8a29f9f798bceb2253264d0a80341a643a6d7ea5","datavalue":{"value":"https://research.tue.nl/nl/publications/a-tracebased-compositional-proof-theory-for-fault-tolerant-distributed-systems(7aab7691-a6e6-433e-aa25-e9d4645e2ccd).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q1330425$81EE9E08-6E0B-41F0-B338-DE3AA29031F0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"67d639d252483be956ab7c56f532a692ae58beae","datavalue":{"value":"A compositional network proof theory for specification and verification of safety properties of fault-tolerant distributed systems is presented. Modeling the effects of faults on the external systems behaviour, i.e. their input/output, is focused. The relation between the system's regular behaviour in case no failure occurs and its acceptable behaviour under failure occurrence is formulated as a failure hypothesis. The paper considers only safety properties, ignoring liveness issues. The propagated method is compositional to allow reasoning with the specifications of processes while ignoring their implementation details.   Examples are given applying the method to a triple-modular redundant system and the alternating bit protocol.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1330425$8BB3584B-8CFC-4A4F-AAB6-6ACF8BCE88BE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$E45668A4-69C4-4730-83DD-6D1FDBC7925D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b65efe51b183d0f4a672427b8171cd1e14211cba","datavalue":{"value":"68W15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$3BF4D0BA-F4B5-4BF9-98B7-E9E2AE894AA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$885F0A33-C8ED-4AAE-A63F-66E7C8978DB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8d8a22ace48964288ca1ed080fca5299ff532395","datavalue":{"value":"68M15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$BC81069E-2BB4-4EA0-9130-49C5C47A3221","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"21711248125d8cb754e206ed1ba56ff627ccc3f4","datavalue":{"value":"609565","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$58235002-BCB0-43E6-AF93-A59DE005DF26","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47511de611e7ca7c7f052290389ebfdae4c32892","datavalue":{"value":"specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1330425$F6F1AB1D-8F5D-4B17-BE9D-16290E52E449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1330425$AD899D3B-9617-4112-8CBE-A1720629CF75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95047b7af8b3eadd827153cb8509157cec754983","datavalue":{"value":"fault-tolerant distributed systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1330425$416BBC8F-B820-493F-B1BF-52EB4BB51456","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"38d48c556d15434219410e690b9b52b5d02dd4a7","datavalue":{"value":"triple- modular redundant system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1330425$F9C76365-BF51-4AB2-A97E-DC4EB744439F","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f8ff4e37ca923917187ada05cf5d58be49dce50","datavalue":{"value":{"entity-type":"item","numeric-id":1742377,"id":"Q1742377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$FF0C3035-0688-4DDB-8384-E9EEA18D1C72","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":"Q1330425$9DF30368-F741-4118-8DA4-023A068CFB40","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"baaca4adc598c94b45402b9d1c05571ec93a33ad","datavalue":{"value":"W2020263005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1330425$F0883BFF-4107-4421-852F-42323D402C7D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$72092CFB-B37D-4FEB-B06C-89C11240DC17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"004642c985382b5c70e78b542aebcb6240614609","datavalue":{"value":{"entity-type":"item","numeric-id":4162644,"id":"Q4162644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$65C48900-200A-4401-9D13-3C4F1DA5B5C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"855be14fb53cf1655d81fe8552b83c8c97789269","datavalue":{"value":{"entity-type":"item","numeric-id":396986,"id":"Q396986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$560EB4C2-EE5F-4229-B88F-8A648F7609C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1c277393b9383fcd1dc49a7b9f8d3b839eb3381","datavalue":{"value":{"entity-type":"item","numeric-id":3994557,"id":"Q3994557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$F29DF79D-B01F-4925-8042-15CF2D515ABE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d1bfc73cddaf2fd9ed4483fd6b40a78290e1de6","datavalue":{"value":{"entity-type":"item","numeric-id":1090102,"id":"Q1090102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$B917F542-50C4-4C43-921C-FB4D7CA9A915","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"151976365c83d6231cc983d63e643b402b6bf6d5","datavalue":{"value":{"entity-type":"item","numeric-id":1085970,"id":"Q1085970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$C3BD9EEF-69D9-4301-8100-866AF5419D1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6816521dd3c4baf1686056439f097d0f1b926044","datavalue":{"value":{"entity-type":"item","numeric-id":3998465,"id":"Q3998465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$894C4B8F-81CF-482B-BA62-B95129E03B13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a55640948606ebada864a0eb07c1b55e76a36f26","datavalue":{"value":{"entity-type":"item","numeric-id":1176075,"id":"Q1176075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$1DB6A941-84C6-4742-B17A-7F0ED00CDDB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcea52628e44d8eb0f4dafe059475aef6acd0444","datavalue":{"value":{"entity-type":"item","numeric-id":1176076,"id":"Q1176076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$56AF25BB-8505-4C54-8B3C-736D1A09F2B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51a6bdb1bc7f6274de02514d257e8687c0fe53a2","datavalue":{"value":{"entity-type":"item","numeric-id":4155798,"id":"Q4155798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$25802AFA-8B8A-4031-9A4C-867670E3D688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a37e9c7e369f220903238ddadd6dceb0a269279","datavalue":{"value":{"entity-type":"item","numeric-id":1330425,"id":"Q1330425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$AC0F2C83-1CDA-4859-BF00-BD6950FEA584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb2e9aeb250aee552f9c7acabe3d57da193b2393","datavalue":{"value":{"entity-type":"item","numeric-id":1187626,"id":"Q1187626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1330425$E1DAA6E8-FB51-4B6C-A37F-CB630A4A4233","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eee4294e71cb3b66235c64fdb14d02d42c0ec26b","datavalue":{"value":{"entity-type":"item","numeric-id":4560363,"id":"Q4560363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87fcd097fec63d66b09ce0c9d10e9b548c0c40d6","datavalue":{"value":{"amount":"+0.9338599","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$1A399E4B-843E-4D02-9129-C213AF88DA27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5f31e86f45c563be4a57d58b223ba48252e7aae","datavalue":{"value":{"entity-type":"item","numeric-id":1085970,"id":"Q1085970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d04e302d874fb5c544a6522f19fdbc428e959d5","datavalue":{"value":{"amount":"+0.9093969","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$D7991644-0C90-4D86-8EC7-DF8C863CD01C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32044f3fb51ddb3f58f94d35bdbb3753cc44f9ad","datavalue":{"value":{"entity-type":"item","numeric-id":5464653,"id":"Q5464653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59bd3df1137f86508d90707c9b2f3acfd1113f77","datavalue":{"value":{"amount":"+0.89014524","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$5B90C17E-AF77-421C-82DA-DC17D61CAEF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0858596335dd9b5a37f9042971ac2431298c3c9f","datavalue":{"value":{"entity-type":"item","numeric-id":4723289,"id":"Q4723289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a88e9b9a0968897feb7c5cfd9a1c946eb5ab47d1","datavalue":{"value":{"amount":"+0.8862516","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$1298078C-AE58-4D22-8C93-01BA989F44E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7d7045f2d31c534448bdcd51e9fe2bbe8f64104","datavalue":{"value":{"entity-type":"item","numeric-id":757079,"id":"Q757079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7579c51ae98789a8401a0bf2d627263f8c1171f3","datavalue":{"value":{"amount":"+0.88459927","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$5592A12E-E109-4EB3-AD6C-8FCDB804DC19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfe49d99b6dd269c73fcd490736ce94023db42d3","datavalue":{"value":{"entity-type":"item","numeric-id":4910418,"id":"Q4910418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44f80ac64299a6bb75c0c783b3f183b21b0e78b0","datavalue":{"value":{"amount":"+0.88410395","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$366030A4-9AB1-40D7-8477-3C20DC56E54B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ff37d49902b9d5663ee08fe8164dedca9a14e82","datavalue":{"value":{"entity-type":"item","numeric-id":1106014,"id":"Q1106014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f20633ef7110ba914b435d9a3bba08d6a77aba7","datavalue":{"value":{"amount":"+0.88353205","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$D7632DF1-B2C7-4CE2-9D88-3007D201EA03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"344c9f9e26dabad61dc24359e63238d6f7ec89f2","datavalue":{"value":{"entity-type":"item","numeric-id":3678655,"id":"Q3678655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20f14c47ffd7816f0b9e8dc2bafd52342d85fa0c","datavalue":{"value":{"amount":"+0.8835319","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1330425$AAF81B14-637D-4C8C-818C-AFFCD9574536","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1330425","badges":[]}}}}}