Layered reasoning for randomized distributed algorithms (2012).

Content Provider	CiteSeerX
Author	Swaminathan, Mani Katoen, Joost-Pieter Olderog, Ernst-Rüdiger
Abstract	This paper adopts the communication closed layer (CCL) concept of Elrad and Francez to the formal reasoning of randomized distributed algorithms. We do so by enriching probabilistic automata (PA) with a layered composition operator, an intermediate between parallel and sequential composition. Layered composition is used to establish probabilistic counterparts of the CCL laws that exploit independence and / or precedence conditions between the constituent PA. The probabilistic CCL laws enable partial order (po-) equivalence when layered composition is replaced by sequential composition. Such po-equivalence induces a purely syntactic partial-order state space reduction via layered separation in compositions of PA while preserving probabilistic next-free linear-time properties. The feasibility of such layered separation is demonstrated on a randomized mutual exclusion algorithm by Kushilevitz and Rabin, complementing an algebraic approach (for analyzing this algorithm) by McIver, Gonzalia, Cohen, and Morgan.
File Format	PDF
Journal	Formal Aspects of Computing
Publisher Date	2012-01-01
Access Restriction	Open
Subject Keyword	Randomized Distributed Algorithm Sequential Composition Layered Separation Distributed Algorithm Probabilistic Ccl Law Randomized Mutual Exclusion Algorithm Syntactic Partial-order State Space Reduction Algebraic Approach Probabilistic Next-free Linear-time Property Ccl Law Partial Order Probabilistic Automaton Probabilistic Counterpart Layered Composition Operator Constituent Pa Formal Reasoning Po-equivalence Induces
Content Type	Text
Resource Type	Article