{"entities":{"Q1079944":{"pageid":1090696,"ns":120,"title":"Item:Q1079944","lastrevid":66823536,"modified":"2026-04-12T13:06:20Z","type":"item","id":"Q1079944","labels":{"en":{"language":"en","value":"Verification of multiprocess probabilistic protocols"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3965421"}},"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":"Q1079944$0D830977-32A6-43AD-AD8D-B7B3BB44D804","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"03e4b70e2d05c108d5de816068cdc8dffff2ee02","datavalue":{"value":{"text":"Verification of multiprocess probabilistic protocols","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1079944$A2A77CF7-A062-4EA5-BFF2-D5FD01C65870","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1899811910a963afa90d4d17efe74d46e059f48f","datavalue":{"value":"0598.68019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1079944$E04E9A8D-557B-4E75-B5FB-397D5067BFCA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b15586fe4070a0c2dc25d6358e64cc9642a64f0d","datavalue":{"value":"10.1007/BF01843570","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1079944$C50798C6-5118-4715-BC66-70073ABB3428","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f609d14c1727f970ab5a0ef43992b4a7d4a23fcd","datavalue":{"value":{"entity-type":"item","numeric-id":208770,"id":"Q208770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$8F040862-3820-470E-802D-E4C41C7BAF02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"12c17a78388b1f2e92062c88fa4de25086298b5f","datavalue":{"value":{"entity-type":"item","numeric-id":439947,"id":"Q439947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$79AAC9D7-08B8-4573-A9A9-4871CC9F1665","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":"Q1079944$1E03168C-F59D-4289-A5DD-3B64C428AEAA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1079944$D5675C77-83B2-45CF-A27A-CED9AB472578","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ab61ca74c97b9f28228b97755e1e3b1d0b94a0dc","datavalue":{"value":"In this paper we demonstrate the utility of temporal logic to the formal verification of probabilistic distributed programs. The approach taken is to represent the quantitative notion of probabilistic computations by the qualitative abstraction of extreme fairness. The method is illustrated first on the dining philosophers problem and then on a new probabilistic symmetric solution to the n-processes mutual exclusion problem. Two related solutions are presented corresponding to different assumptions about the granularity of a compound test.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$CEB73AE3-0106-4C60-8624-09794C4F5CF2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1079944$DD2600AE-7760-4FDC-B784-DD12327B4E5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1079944$D787C8EF-94D1-4109-BEED-562C6E7D29E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f3a228ae5bcbee654814c5a44d75053eaa669c69","datavalue":{"value":"3965421","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1079944$6A1D07EA-EE37-4749-B96E-8EF873816ABD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$B113C7AB-FADC-4633-8AC7-286EA5096347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cbb95103fc3fc04c3b210a52bb9e7acd7620b8b7","datavalue":{"value":"formal verification of probabilistic distributed programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$4ECD68F2-A27E-4CEA-8796-9C186C4B3302","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e3484d7015c933cc3c61f484950aa68e1a28621","datavalue":{"value":"probabilistic computations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$AD989FB9-A867-434F-852A-67CDEA5CE4AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08247d2e53e3c0d7ab77ca353aebcd191ca2cbd1","datavalue":{"value":"extreme fairness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$B006DE4E-E590-41BE-A079-98F2C4F0DE27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7bfb923eb8ccce9882476d98309ef82969d2df52","datavalue":{"value":"dining philosophers problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$5D4C220F-3BBB-43C1-9AA1-296F95A40D1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa81da7ff1ef8af264d810c7b287d951f19df664","datavalue":{"value":"n-processes mutual exclusion problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1079944$CD6B14C5-3C7D-4F49-A02E-2F5BFEC399C2","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":"Q1079944$0989599B-0CD2-46EF-B02F-966ADA1E388A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f89ecac9343e8f2e3e23ab0f8f3d38e86277832","datavalue":{"value":{"entity-type":"item","numeric-id":1348531,"id":"Q1348531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$8AF43594-1681-4FB4-B8F1-5E92A697A7E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2e80321a5b901dd6bcf10e15a0ea7c4a4a661ba","datavalue":{"value":{"entity-type":"item","numeric-id":4749184,"id":"Q4749184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$383A13A1-AD54-41FE-8902-199FBFD0A1A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4c9a168cfecebbdce77004f3cafd3d6265c7163","datavalue":{"value":{"entity-type":"item","numeric-id":3674620,"id":"Q3674620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$03E90694-8184-44EF-92DB-0B684460A4FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a905ba949a06cde66174f0d589d9794d6c05423","datavalue":{"value":{"entity-type":"item","numeric-id":3711745,"id":"Q3711745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$1ABBFA22-85B7-4014-836F-6B4933822BB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5b4c95f53b57f2eb31607a9241c4b370cdcd831","datavalue":{"value":{"entity-type":"item","numeric-id":3939208,"id":"Q3939208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$146B30A3-89CE-46AC-A428-D09DC1F3206D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e09f7681257b92526d42b556170b42e07509410","datavalue":{"value":{"entity-type":"item","numeric-id":4745241,"id":"Q4745241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$D29ED783-0069-4BB6-B8E5-943FA0D76111","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":"Q1079944$E685387B-704C-4044-B41B-BE231372267D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8f955881ec719424b635d12ed43cbd0176010fe","datavalue":{"value":{"entity-type":"item","numeric-id":1162148,"id":"Q1162148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$46E05A4B-C147-4C90-ACE1-F71E176193DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97ff44c4c36fb63b7548b031016090932a6a0251","datavalue":{"value":{"entity-type":"item","numeric-id":3674052,"id":"Q3674052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1079944$D4F447C8-BAB3-4B02-8F5C-8E10EBDDACC5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"356d37e5aedcdbcde1449423060cf5f806a07079","datavalue":{"value":{"entity-type":"item","numeric-id":916356,"id":"Q916356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d19831ec030a76c6f7439f1b94fec0573f23266b","datavalue":{"value":{"amount":"+0.9196546","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$FE1C414C-4694-4062-A70B-C4E3C01BF5C5","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":"5fd87420d24039ee842857d01a90dd221bc6f21d","datavalue":{"value":{"amount":"+0.91669774","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$34CFAC79-CCC8-4D7E-8404-C89084FB0D22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5f4034399829c7be670eedad7e312c427b8bd41","datavalue":{"value":{"entity-type":"item","numeric-id":5465856,"id":"Q5465856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2edc3478987bff04b71f1094fd31994664660ea0","datavalue":{"value":{"amount":"+0.9085021","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$198DBC19-59A6-4FED-B424-9662494BD154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9c2f2a7fc8474c0133780afda7d6c98adfa044d","datavalue":{"value":{"entity-type":"item","numeric-id":3316558,"id":"Q3316558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"669d3f3620f8ab5a9dc96adf1e428ced41152297","datavalue":{"value":{"amount":"+0.90501267","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$5D805561-CE18-4803-A8CA-7A51EEA7A7BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"acc116bba91a1424430dd64c9629324bd6668e40","datavalue":{"value":{"entity-type":"item","numeric-id":2573634,"id":"Q2573634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16340df74ea11cb376c743f6c4a42a0d6c28715f","datavalue":{"value":{"amount":"+0.90313804","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$6240CBA9-96A5-413A-80F2-3B4E32B488D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b6902b274976c6d6a70806a30b31dec7571c52e","datavalue":{"value":{"entity-type":"item","numeric-id":4417850,"id":"Q4417850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16340df74ea11cb376c743f6c4a42a0d6c28715f","datavalue":{"value":{"amount":"+0.90313804","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$1C349AF4-50C0-4A7B-AF84-2441E3317469","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"709267e3c465aee249444b8785b4862aa5af1286","datavalue":{"value":{"entity-type":"item","numeric-id":2963938,"id":"Q2963938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9a89841abbf54e8752c10beccdb833bda1675c9","datavalue":{"value":{"amount":"+0.901105","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$B7F146FC-B55A-4370-AD9D-CFB59EBD9FB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4daf2a2810634fe6ebc122ee210d088e3b897775","datavalue":{"value":{"entity-type":"item","numeric-id":1849556,"id":"Q1849556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ed96279b03ccfd350665509e9f7dee8dc2e51b7","datavalue":{"value":{"amount":"+0.8966075","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$10E32536-FCE0-45C5-8863-BF0CC2FFD899","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f65aeaf270c79045138cdcef76a78547e5739e3c","datavalue":{"value":{"entity-type":"item","numeric-id":2938068,"id":"Q2938068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0212271362fda3b3b3b6511610162f929c59847","datavalue":{"value":{"amount":"+0.8933742","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1079944$512B57B4-7AAE-43B7-A0C7-EABCA8046464","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verification of multiprocess probabilistic protocols","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verification_of_multiprocess_probabilistic_protocols"}}}}}