2011/07/29 by José Proença, Dave Clarke, Erik de Vink +1 · 11 citations
Computer Science · #Automaton #Coordination game #Data exchange #Distributed systems and fault tolerance #Formal Methods in Verification #Linearizability #Logic, programming, and type systems #Predicate (mathematical logic) #Scalability #cs.FL #cs.LO #cs.SE
paper · pdf · doi:10.4204/eptcs.58.5
published in Electronic Proceedings in Theoretical Computer Science 58, 65-79 (Open Publishing Association) · In Proceedings FOCLASA 2011, arXiv:1107.5847
openalex publication_date 2011/07/29 · arxiv created 2011/08/01 · arxiv updated 2011/08/02 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/06
Synchronous coordination systems allow the exchange of data by logically indivisible actions involving all coordinated entities. This paper introduces behavioural automata, a logically synchronous coordination model based on the Reo coordination language, which focuses on relevant aspects for the concurrent evolution of these systems. We show how our automata model encodes the Reo and Linda coordination models and how it introduces an explicit predicate that captures the concurrent evolution, distinguishing local from global actions, and lifting the need of most synchronous models to involve all entities at each coordination step, paving the way to more scalable implementations.