After an extensive Introduction, we fix most basic notation and terminology used throughout this thesis in Chapter 2. Consequently, in Chapter 3 we define the automata as used in this thesis and we review some notions from automata theory.

In Chapter 4 we define how to combine a set of automata in order to form a synchronized automaton. We also define how to obtain a subautomaton from a synchronized automaton as a subset of its constituting automata, and we study the relation between synchronized automata and their subautomata in terms of computations. Consequently, we show how to compose synchronized automata in an iterative way. Within synchronized automata we then characterize three basic and very natural ways of synchronizing on shared actions of their constituting automata, which form the basis of the more complex types of synchronization we introduce later. Finally, we define unique synchronized automata being maximal with respect to a given type of synchronization. Through the formulation of predicates of synchronization we moreover provide direct constructions of such synchronized automata.

In Chapter 5 we define team automata as compositions of component automata, i.e. from now on we distinguish input, output, and internal actions. To this aim we use the foundation layed in the preceding chapters and build team automata and component automata on top of (synchronized) automata. We then build subteams on top of subautomata, and we study the relation between team automata and their subteams. Also in the case of team automata, we show how to compose them in an iterative way. We then build several complex types of synchronization on top of those introduced in the previous chapter, by using the different roles that an action may have in the various component automata. Similar to synchronized automata, we define unique team automata being maximal with respect to particular types of synchronization. Through the formulation of predicates of synchronization we furthermore provide direct constructions for such team automata.

In Chapter 6 we study the computations and behavior of team automata in relation to those of their constituting component automata. Therefore we study (synchronized) shuffles and their properties. We prove that the behavior of certain team automata can be described in terms of certain (synchronized) shuffles of the behavior of their constituting component automata.

In Chapter 7 we provide a comparison of team automata with two other models. The first is I/O automata, of which team automata are an extension. The second is a model based on Petri nets, for which we define team automata with vector actions as an extension of team automata.

In Chapter 8 we present three examples demonstrating the usefulness of team automata in practical settings. We first show how to model a specific groupware architecture by team automata. Secondly, we show how team automata can be employed to model collaboration between teams of developers engaged in the development of models of complex (software) systems. Thirdly, we show how various known access control strategies can be given a rigorous formal description in terms of synchronizations in team automata.

In the Discussion, finally, we recall the main contributions of this thesis and point out some topics worth further investigation. Furthermore, we indicate how - in theory - team automata can be used for system design and where - in practice - they have actually been used.