Paper Info
Title
Layered reasoning for randomized distributed algorithms
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.
Year
DOI
Venue
2012
10.1007/s00165-012-0231-x
Formal Asp. Comput.
Keywords
Field
DocType
layered composition operator,probabilistic counterpart,layered separation,constituent pa,probabilistic next-free linear-time property,probabilistic ccl law,layered composition,layered reasoning,probabilistic automaton,sequential composition,ccl law
Formal reasoning,Algebraic number,Computer science,Algorithm,Theoretical computer science,Distributed algorithm,Composition operator,Equivalence (measure theory),Probabilistic logic,Mutual exclusion,Probabilistic automaton
Journal
Volume
Issue
ISSN
24
4-6
1433-299X
Citations 
PageRank 
References 
4
0.41
22
Authors
3
Name
Order
Citations
PageRank
Mani Swaminathan1583.79
Joost-Pieter Katoen24444289.65
Ernst-Rüdiger Olderog3682220.84