Synchronized shuffles

We introduce and investigate three synchronized shuffle operations on words and languages. We show how such operations come into play when proving compositionality of automata-based specification models, by demonstrating their usage in the context of team automata. As far as the mathematical properties of these operations are concerned, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied in this paper. Finally, based on this result, we present an algorithm for deciding whether or not a given regular language is synchronized shuffle closed.