Constraint Automata
Baier, Sirjani, Arbab & Rutten’s (2006) compositional formal semantics for Reo connectors: each connector denotes a finite automaton whose states capture buffer / memory contents and whose transitions specify which subsets of endpoints synchronise simultaneously and what data passes. Composition of connectors is the synchronous product of their constraint automata. Provides a tractable semantic basis for verification, model-checking, and the equational theory of Reo connectors.