A calculus for team automata

Team automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patterns among distributed systems, extending classical I/O automata. Furthermore, for some of these patterns, the language recognised by a team automaton can be specified in terms of the languages recognised by its components. The present paper introduces a process calculus tailored over team automata. Each automaton is thus described by a process, in such a way that its associated (fragment of a) labelled transition system is bisimilar to the original automaton. Furthermore, the mapping is proved to be denotational, since the operators on processes are in a bijective correspondence with a chosen family of coordination patterns, and that correspondence is preserved by the mapping. The paper thus extends to team automata some classical results on I/O automata and their representation by process calculi. Moreover, besides providing a language for expressing team automata and their composition, we widen the family of coordination patterns for which an equational characterisation of the language associated to a composite automaton can be provided. The latter result is obtained by providing a set of axioms, in ACP-style, for capturing bisimilarity in our calculus.