A Partial Order View of Message-Passing Communication Models
summary
Presents a unified hierarchy of seven communication models from fully asynchronous to realizable with synchronous communication and proves each model is MSO axiomatizable so behaviors become graphs amenable to monadic second order logic. Shows decidability of containment when a class C is MSO definable and has bounded special treewidth and uses that to recover model checking via bounded special treewidth. Delivers specific decidability results, one remaining open case for weakly synchronous under fully asynchronous semantics, and a web MSC validator prototype.
AI-written summary · about
chapters (4)
related talks
22mAutomated reasoning on consistency models with MONA
20mImplementability of Global Distributed Protocols Modulo Network Architectures
20mMessage-Observing Sessions
20mModel Checking Distributed Protocols in Must
58mThe Communication Complexity Landscape of Information-theoretic MPC
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
35mCommunicating Sequential Processes
20mDeciding Asynchronous Hyperproperties for Recursive Programs