{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:11:18Z","timestamp":1762297878480},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2012,7,1]],"date-time":"2012-07-01T00:00:00Z","timestamp":1341100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2012,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-012-0231-x","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"477-496","source":"Crossref","is-referenced-by-count":8,"title":["Layered reasoning for randomized distributed algorithms"],"prefix":"10.1145","volume":"24","author":[{"given":"Mani","family":"Swaminathan","sequence":"first","affiliation":[{"name":"University of Oldenburg, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[{"name":"University of Oldenburg, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Attiya H Censor K (2008) Tight bounds for asynchronous randomized consensus. J ACM 55(5)","DOI":"10.1145\/1411509.1411510"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Baier C Gr\u00f6\u00dfer M Ciesinski F (2004) Partial order reduction for probabilistic systems. In: Quantitative evaluation of systems (QEST) IEEE CS Press pp 230\u2013239","DOI":"10.1109\/QEST.2004.1348037"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-007-0032-1"},{"key":"e_1_2_1_2_4_2","first-page":"45","volume-title":"Mathematics of program construction (MPC), volume 1837 of LNCS.","author":"Cohen E","year":"2000"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio PR. Niebert P (2004) Partial order reduction on concurrent probabilistic programs. In: Quantitative evaluation of systems (QEST). IEEE CS Press pp 240\u2013249","DOI":"10.1109\/QEST.2004.1348038"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Janssen W Zwiers J (1992) From sequential layers to distributed processes: deriving a distributed minimum weight spanning tree algorithm. In: Principles of distributed computing (PODC). ACM Press pp 215\u2013227","DOI":"10.1145\/135419.135461"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska MZ Norman G (2002) Verifying randomized Byzantine agreement. In Peled D Vardi MY (eds) Formal description techniques (FORTE) volume 2529 of LNCS. Springer pp 194\u2013209","DOI":"10.1007\/3-540-36135-9_13"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"e_1_2_1_2_10_2","volume-title":"Theorie der Endlichen und Unendlichen Graphen: Kombinatorische Topologie der Streckenkomplexe","author":"Koenig D","year":"1936"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Kushilevitz E Rabin MO (1992) Randomized mutual exclusion algorithms revisited. In: PODC pp 275\u2013283","DOI":"10.1145\/135419.135468"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.021"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Lehmann DJ Rabin MO (1981) On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Principles of programming languages (POPL). ACM Press pp 133\u2013138","DOI":"10.1145\/567532.567547"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.10.005"},{"key":"e_1_2_1_2_15_2","volume-title":"Communication and concurrency","author":"Milner R","year":"1989"},{"key":"e_1_2_1_2_16_2","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"McIver AK","year":"2004"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799364006"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Olderog E-R Swaminathan M (2010) Layered composition for timed automata. In: Chatterjee K Henzinger TA (eds) Formal modeling and analysis of timed systems (FORMATS) volume 6246 of LNCS. Springer pp 228\u2013242","DOI":"10.1007\/978-3-642-15297-9_18"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/PL00008917"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90010-1"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Saias I (1992) Proving probabilistic correctness statements: the case of Rabin\u2019s algorithm for mutual exclusion. In: Principles of distributed computing (PODC). ACM Press pp 263\u2013274","DOI":"10.1145\/135419.135466"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03259394"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Segala R (2000) Verification of randomized distributed algorithms. In: Brinksma E Hermanns H Katoen J-P (eds) Formal methods and performance analysis volume 2090 of LNCS. Springer pp 232\u2013260","DOI":"10.1007\/3-540-44667-2_6"},{"issue":"2","key":"e_1_2_1_2_24_2","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala R","year":"1995","journal-title":"Nordic J Comput"},{"key":"e_1_2_1_2_25_2","first-page":"176","article-title":"An introduction to probabilistic automata","volume":"78","author":"Stoelinga M","year":"2002","journal-title":"Bull EATCS"},{"key":"#cr-split#-e_1_2_1_2_26_2.1","doi-asserted-by":"crossref","unstructured":"Stoelinga M Vaandrager FW (1999) Root contention in IEEE 1394. In: Katoen J-P","DOI":"10.1007\/3-540-48778-6_4"},{"key":"#cr-split#-e_1_2_1_2_26_2.2","unstructured":"(ed) AMAST workshop on real-time and probabilistic systems (ARTS) volume 1601 of LNCS. Springer pp 53-74"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Timmer M Stoelinga M van de Pol J (2011) Confluence reduction for probabilistic systems. In: Abdulla PA Leino KRM (eds) Tools and algorithms for the construction and analysis of systems (TACAS) volume 6605 of LNCS. Springer pp 311\u2013325","DOI":"10.1007\/978-3-642-19835-9_29"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0231-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0231-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0231-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:53Z","timestamp":1641484733000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0231-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":28,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0231-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0231-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}