Publications on Team Automata

(People) Using Team Automata

A Tool to Compose Team Automata (*written by Jonas Casanova*)

For the time being it can only
compose according to the basic synchronization strategies free, ai
and si, and for small/medium-sized systems. A small tutorial is
included in the distribution.

Teamautomaten |

Team automata form a mathematical framework introduced in [Ell97] to model components of groupware systems and their interconnections. The usefulness of team automata however extends to modeling collaboration between system components in general (for an overview, see e.g. [Bee03] and [BLP05]).

A system is *reactive* if, in order for it to function, it has a
continuous need to interact with its environment. Its functioning thus
depends on the functioning of its environment. This contrasts with a system
that is *transformational*, in which case its functioning (output) is
merely a function of its input. Examples of reactive systems include computer
operating systems and coffee vending machines, whereas a compiler is an
example of a transformational system.

Groupware systems are systems intended to support groups of people working together in collaborative projects. Such systems are often distributed and reactive, and conceived as consisting of components cooperating in a coordinated way. This leads to complex interactive behavior and, consequently, coordination policies and their effect on behavior are key issues within CSCW. At a conceptual level CSCW needs a precise, consistent, and unambiguous terminology, while at a lower, architectural level CSCW has been searching for a rigorous mathematical framework to specify and verify groupware systems.

The model of *Input/Output automata* (I/O automata for short) was
introduced by M.R. Tuttle in 1987 for the specification and verification of
distributed reactive systems and consequently elaborated upon by M.R. Tuttle
and N.A. Lynch. I/O automata served as the theoretical source of inspiration
for the introduction of team automata in [Ell97] through the distinction of
the model's actions into input, output, and internal actions. We come back to
this shortly. A conceptual source of inspiration for team automata was the
1994 book "Collective Intelligence in Computer Based Collaboration", in which
J. Smith conjectures that well-structured groups (called teams) outperform
individuals in certain tasks, but at the same time calls for models capturing
concepts of group behavior.

In [Ell97] team automata were introduced explicitly for the specification and verification of groupware systems and they were shown to be promising at both the conceptual and the architectural level of groupware systems. Subsequently it has been demonstrated that the usefulness of team automata is not limited to clarifying and capturing precisely notions related to collaboration between components of groupware systems, but extends to other kinds of (reactive) systems.

A team automaton is composed of *component automata*, which are a
special type of *automata*. The crux of composing a team automaton is
to define the way in which those originally independent component automata
interact. Their interactions are formulated in terms of
*synchronizations* of shared actions, a method for modeling
collaboration among system components well known from the literature.

Assume that we have an automaton modeling a coffee vending machine. Then a possible event is a user inserting a coin, which when it occurs leads to a state change of the automaton. The user forms a part of the environment of the coffee vending machine. A coffee vending machine is thus an example of a reactive system, with the insertion of coins by a user as interactions with its environment.

Next assume that also the user is modeled by an automaton, with the insertion of a coin as one of its actions. Then we have two automata, both equipped with an action modeling the insertion of a coin. When composing these two automata into one system, inserting a coin into the coffee vending machine appears as a single synchronized action. In the composed system the occurrences of an action from the automaton modeling the user and the same action from the automaton modeling the coffee vending machine are identified, i.e. simultaneously executed by the two system components. The transitions of a thus composed automaton will be synchronized occurrences of transitions of its constituting automata that have the same action label.

An automaton does not necessarily participate in every synchronization of an action it shares. Hence there is no such thing as the unique synchronized automaton over a set of automata. Rather, a whole range of synchronized automata, distinguishable only by their transition relation, can be constructed from a given set of automata. It is this freedom to choose a transition relation that sets the team automata framework apart from most other models. Another distinguishing feature of this framework is the fact that the transitions of a synchronized automaton are labeled with one single action. We come back to this shortly.

From the way a synchronized automaton is constructed it is clear that it is itself an automaton again. Consequently, it can serve as a constituting automaton of a higher-level synchronized automaton, thus allowing hierarchical designs.

Within a synchronized automaton, three natural types of actions can be
distinguished, based on the way they appear in synchronizations. Actions
that are never executed simultaneously by more than one constituting
automaton are *free*. Actions that are always executed as
synchronizations in which all automata participate that have this action
in their alphabet are called *action-indispensable*.
*State-indispensable* actions, finally, require the participation of
only those automata that are ready (in a suitable state) to execute that
action.

A team automaton over a set of component automata is defined in a way similar to the definition of synchronized automata. As before, its (initial) states are cartesian products of (initial) states of its constituting component automata. Its actions are the actions of its constituting component automata, now distributed over input, output, and internal actions. All internal (output) actions of the component automata remain internal (output) actions of the team automaton. The remaining actions are those input actions of the component automata that do not occur as an output action of any of the component automata, and they become the input actions of the team automaton. Its labeled transitions, finally, are - as before - synchronizations of labeled transitions of its constituting component automata.

Like in the case of synchronized automata, we do not require all constituting component automata sharing an action to participate in every synchronization of that action. Synchronizations of internal actions never involve more than one component automaton because every internal action uniquely belongs to one particular component automaton. Moreover, independently of the states of the other component automata, an internal action can always be executed as before the composition. Like in the case of synchronized automata, there is no unique team automaton. Rather a whole range of team automata, distinguishable only by their transition relation, can be constructed.

The reason given in [Ell97] for equipping team automata - like I/O automata -
with a distinction of actions into input, output, and internal actions, is the
explicit desire to model different types of synchronization. This is achieved
by taking the different role (input, output, or internal) that actions can
have in different component automata into account. External actions may be
input to some component automata and output to other component automata. In
*peer-to-peer* synchronizations, actions have the same role in each of
the component automata involved. In such synchronizations, all component
automata are on equal footing with respect to the action being synchronized.
This differs from *master-slave* synchronizations, in which input
actions ('slaves') are driven by output actions ('masters'), i.e. the slaves
have to follow the masters.

Team automata form a very broad and generic framework. Component automata can cooperate in many possible ways through synchronizations of shared actions. The freedom of choosing the transition relation of a team automaton moreover offers the flexibility to distinguish even the smallest nuances in the meaning of one's design. Leaving the set of transitions of a team automaton as a modeling choice thereby becomes one of the most important features of team automata.

First, the set of actions of a team automaton consists of input, output, and
internal actions, thus allowing the classification of a broad range of often
complex synchronizations in team autamata. This distinction of input, output,
and internal actions originates from two independently developed models: I/O
automata and the *I/O systems* introduced by B. Jonsson in 1987. Since
the semantics of an I/O system - given in terms of automata - is essentially
an I/O automaton, we will speak only of I/O automata in the sequel. Team
automata are, in fact, an extension of I/O automata (cf. [BK05]).

I/O automata are not the only model in the literature in which a distinction
of actions is used. The same distinction can be found in the I/O automata-based *interface automata* introduced by L. De Alfaro and T.A. Henzinger in 2001, the I/O
automata-based *reactive transition systems* introduced by J. Carmona
and J. Cortadella in 2002, the *interacting state machines*
introduced by D. Oheimb in 2002 (which were introduced specifically for
modeling reactive systems), and the *Component-Interaction automata* (CI automata for short) introduced by L. Brim, I. Cerna, P. Varekova, and B. Zimmerova in 2005 (which were based on interface automata, I/O automata, and team automata). A further example is R. Milner's *CCS*. In
CCS, the internal or *silent action* τ
is a distinguished element of the set of actions. It denotes the 'perfect'
action of a *handshake communication*, i.e. the synchronization of two
*complementary (input and output) actions*.

Secondly, the transitions of a team automaton are synchronizations of
transitions with the same label. The simultaneous execution of actions from
a team automaton's constituting component automata is thus limited to common
actions. We call such types of synchronization *uniform* in order to
distinguish them from *pluriform synchronizations* in which distinct
actions can be executed simultaneously.
Also this feature of allowing solely uniform synchronizations originates from
the I/O automaton model, and it thus holds also for the above I/O automata-based formalisms. These are by far not the only models in the literature
prohibiting pluriform synchronizations. Other examples include the *mixed
product* over a set of automata introduced by C. Duboc in 1986. A further
example is the theory of *path expressions*, which was consequently
encompassed in the *COncurrent SYstems* (COSY for short) notation and
given a *vector firing sequence* semantics, which considers *vector
actions* rather than ordinary actions (for details, see the 1992 book
"Specification and Analysis of Concurrent Systems, The COSY Approach" by
R. Janicki and P.E. Laurer). An entry of such a vector action is not empty
if and only if the respective component participates.

There are also examples of automata-based models that do allow pluriform
synchronizations, such as the *free product* and the *synchronous
product* over a set of automata. Both were defined as the culmination of
a framework of process models proposed by M. Nivat and A. Arnold in a number
of papers and course notes from 1979 onwards. Another example is the framework
of *Vector Controlled Concurrent Systems* (VCCSs for short) introduced
by N.W. Keesmaat, J. Kleijn, and G. Rozenberg in 1990 as generalizations of
the COSY theory. These systems introduced allow pluriform synchronizations of
actions of its constituting components and execute vectors of actions rather
than ordinary actions.
A subclass of *vector team automata* (i.e. team automata with an explicit representation of synchronizations) can be translated into Individual Token Net Controllers, a model of labeled Petri nets developed within the framework of VCCSs (cf. [BK12]).

Yet another type of synchronization is the handshake communication in CCS
mentioned above. Many algebraic specification languages moreover contain
specific parallel composition operators that allow processes to communicate
through synchronizations. Among the best known such examples is C.A.R. Hoare's
*(T)CSP*.

Thirdly, the transition relation of a team automaton is not uniquely determined by its constituting component automata, which also distinguishes team automata from I/O automata. This freedom of choosing the transition relation of the automaton obtained when composing a set of automata, occurs in the literature as well. An example is the aforementioned synchronous product over a set of automata. Whereas the transition relation of the free product over a set of automata is the set of all possible pluriform synchronizations, that of the synchronous product over that set of automata is the restriction of the free product to the subset of all possible pluriform synchronization vectors defined by a specifically formulated synchronization constraint. This synchronization constraint is formulated in terms of the actions only and does not depend on the current states of the automata. Another example is the CI automata model, which was specifically designed with this feature of team automata.

Most automata-based models, however, use a single and very strict method for
choosing the transition relation of an automaton composed over a set of
automata, in effect resulting in composite automata that are uniquely defined
by their constituents. The choice prevalent in the literature is to include,
for all actions, all and only those transitions in which all automata
participate that have the action in their alphabet. Since this means that all
actions will be action-indispensable, we call this the *ai* principle.
Examples of automata-based models with composition based on the *ai*
principle include the aforementioned mixed product and product automaton over
a set of automata, as well as reactive transition systems, interacting state
machines, and I/O automata. Other examples from the literature - without
claiming completeness - include *cooperating (pushdown) automata* and
*timed cooperating automata*. The *ai* principle furthermore
appears in disguise in non-automata-based models like (T)CSP and D. Harel's
*statecharts*.

Team automata that are unique with respect to particular types of
synchronization have also been defined. Moreover, through the formulation of
predicates of synchronization, direct constructions for such team automata
were provided. However, of all the resulting uniquely defined team automata,
it is precisely the one based on the *ai* principle that possesses the
at first sight most appealing characteristics. It is important to note that
peer-to-peer and master-slave types of synchronization, which were introduced
with a clear practical motivation in mind, cannot be distinguished in I/O
automata. In fact, in a team automaton constructed according to the
*ai* principle, all synchronizations are by definition master-slave.

To the best of our knowledge, at the time of their introduction no automata-based model other than team automata
united the three features discussed before. I/O automata satisfy the first two
features, namely the distinction of input, output, and internal actions, and
the prohibition of pluriform synchronizations. However - as already noted by
M.R Tuttle in 1987 - the single notion of automaton composition in I/O
automata is rather restrictive and may hinder a realistic modeling of certain
types of interactions. This is the main motivation given in [Ell97] for
introducing team automata as a generalization of I/O automata. Another
important reason for generalizing I/O automata is the fact that I/O automata
are *input enabling*, i.e. in every state of the automaton every input
action of that automaton can be executed. Though convenient when modeling
reactive computer systems, this hinders a realistic modeling of interactions
that involve humans. Team automata have thus been introduced with the
motivation of creating a single model in which the above three features are
united. Since CI automata were specifically based on team automata, it is not surprising that they also unite the three features discussed above.

Through the classification of a broad range of ways to synchronize actions in team automata, a systematic study of the role that synchronizations play when modeling collaboration between system components has been conducted. To begin with, their effect on the inheritance of various automata-theoretic properties from team automata to their constituting component automata and subteams, and vice versa, has been studied. Furthermore, their effect on the inheritance of various automata-theoretic properties from team automata to their constituting component automata and subteams, and vice versa, has been studied. These studies, presented in [Bee03], however are not complete and thus offer interesting pointers for further investigation.

The relation between team automata and two related models, namely I/O automata and Petri nets, has been investigated in considerable detail in [Bee03], [BK05], and [BK12]. This has shown that I/O automata fit into the framework of team automata, whereas so-called non-state-sharing vector team automata can be translated into Individual Token Net Controllers - a model of vector-labeled Petri nets. Vector team automata are team automata in which the (team) actions have been replaced by vectors of (component) actions, from which the participation of a component automaton in a synchronization can thus be seen immediately. Consequently, non-state-sharing vector team automata are the subclass of vector team automata with the characteristic that whether or not a synchronization can take place only depends on the local states of the component automata actively involved in that synchronization. As a result, synchronizations involving disjoint sets of component automata are independent, which would thus allow a concurrent semantics for non-state-sharing vector team automata. This is a point worth further investigation.

Team automata are naturally suited for component-based system design due to the fact that they can themselves be used as component automata of higher-level team automata. This allows the iterative composition of team automata. In [BEKR03] it has been shown that iterated composition does not lead to an increase of the number of possibilities for synchronization. Every iterated team automaton over a composable system can be interpreted as a team automaton over that composable system, by reordering its state space and transition space. It has moreover been shown that every team automaton can be iteratively composed over its subteams.

In [BK03], the computations and behavior of team automata in relation to those of their constituting component automata has been studied in detail. Several types of team automata that satisfy compositionality could be identified. To describe the compositionality of team automata, it was necessary to develop an extensive theory of (synchronized) shuffles. An examination of the compositionality of further types of team automata is certainly a topic worth further investigation. This might very well require the introduction and analysis of more sophisticated types of shuffles.

In [BK05], is has been shown how Input/Output automata fit in the framework of team automata, thus making it possible to view certain notions and results regarding their modular structure as special instances of more general observations.

In a series of papers (cf., e.g., [BLP05] and [BLP06]), it has been shown that team automata are well suited for the analysis of security aspects in communication protocols. To this aim, an insecure communication scenario for team automata - general enough to encompass various communication protocols - was defined and the Generalized Non-Deducibility on Compositions schema - originally introduced in the context of process algebrae - was reformulated in terms of team automata. Based on the resulting team automata framework, two analysis strategies that can be used to verify security properties of communication protocols were developed. Several case studies have shown how this framework can be used.

In [BGJ06], a process calculus for modelling team automata has been introduced, extending some classical results on I/O automata. As a side result, the family of team automata that guarantees a degree of compositionality has been widened slightly.

Motivated by the abovementioned natural synchronization patterns applied in the composition of team automata, in [BK09] the associativity of different (potentially unfair) synchronized shuffle operations has been investigated. This has led to an extension of the results from [BK03], where compositionality of team automata was considered only in the context of finitary behaviors.

In [BK12], vector team automata have been defined as team automata with an explicit representation of synchronizations and a translation has been given of a subclass of such vector team automata into Individual Token Net Controllers, a model of labeled Petri nets developed within the framework of VCCSs.

Here follows merely a selection (in the order of writing):

- [Ell97]: C.A. Ellis,
Team Automata for Groupware Systems. In
*Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge (GROUP'97), Phoenix, AZ, U.S.A.*(S.C. Hayne and W. Prinz, eds.), ACM Press, New York, 1997, 415--424.

Informally introduces the concept of Team Automata explicitly for the description and analysis of groupware systems and their interconnections. - [BEKR03]:
M.H. ter Beek, C.A. Ellis, J. Kleijn, and G. Rozenberg,
Synchronizations in Team Automata for Groupware
Systems.
*Computer Supported Cooperative Work - The Journal of Collaborative Computing*12, 1 (2003), 21 - 69.

Elaborates further on the concept of team automata by defining them in a mathematically precise way. It is shown how the formal setup allows one to distinguish between several types of synchronization and to classify team automata accordingly. Based on the observation that team automata can be used as components in higher-level teams, it is also shown how the framework allows for the representation of hierarchical systems. - [BEKR01b]:
M.H. ter Beek, C.A. Ellis, J. Kleijn, and G. Rozenberg,
Team Automata for Spatial Access Control. In
*Proceedings of the Seventh European Conference on Computer-Supported Cooperative Work (ECSCW 2001), Bonn, Germany*(W. Prinz, M. Jarke, Y. Rogers, K. Schmidt, and V. Wulf, eds.), Kluwer Academic Publishers, Dordrecht, 2001, 59 - 77.

Demonstrates the model usage and utility for capturing information security and protection structures, and critical coordinations between these structures. On the basis of a spatial access metaphor, various known access control strategies are given a rigorous formal description in terms of synchronizations in team automata. - [EG02]:
G. Engels and L.P.J. Groenewegen,
Towards Team-Automata-Driven Object-Oriented Collaborative Work. In
*Formal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg*(W. Brauer, H. Ehrig, J. Karhumäki, and A. Salomaa, eds.),*Lecture Notes in Computer Science*2300, Springer-Verlag, Berlin, 2002, 257 - 276.

Studies and compares two different approaches to model communication and cooperation, namely team automata and statecharts, yielding some interesting insights. In particular, the differences between action-based, synchronous, and state-based, asynchronous communication are elucidated. - [BCM04]:
M.H. ter Beek, E. Csuhaj-Varjú, and V. Mitrana,
Teams of Pushdown Automata.
*International Journal of Computer Mathematics*81, 2 (2004), 141 - 156.

Introduces team pushdown automata as a theoretical framework capable of modelling various communication and cooperation strategies in multi-agent systems. Team pushdown automata are obtained by augmenting distributed pushdown automata with the notion of team cooperation or - alternatively - by augmenting team automata with pushdown memory. Based on the notion of competence, a variety of team cooperation strategies is introduced. The focus is on the accepting capacity of team pushdown automata, but an application of the enhanced modelling power of team automata obtained through the addition of pushdown memory is hinted at. - [Kle03]:
J. Kleijn,
Team Automata for CSCW - A Survey -. In
*Petri Net Technology for Communication-Based Systems - Advances in Petri Nets*(H. Ehrig, W. Reisig, G. Rozenberg, and H. Weber, eds.),*Lecture Notes in Computer Science*2472, Springer-Verlag, Berlin, 2003, 295 - 320.

A survey of team automata is presented, including a brief comparison with related models like Input/Output automata and models based on Petri nets. - [BK03]:
M.H. ter Beek and J. Kleijn, Team Automata
Satisfying Compositionality. In
*Proceedings of FME 2003: Formal Methods - the 12th International Symposium of Formal Methods Europe, Pisa, Italy*(K. Araki, S. Gnesi, and D. Mandrioli, eds.),*Lecture Notes in Computer Science*2805, Springer-Verlag, Berlin, 2003, 381 - 400.

Presents an initial investigation of the conditions under which team automata satisfy compositionality, in the sense that their behavior can be described in terms of that of their constituting component automata. - [BB03]:
M.H. ter Beek and R.P. Bloem, Model Checking Team Automata for Access Control.
Unpublished manuscript, 2003.

Initiates an attempt to validate some of the specifications resulting from [BEKR01b] with the model checker Spin. - [BLP03]:
M. ter Beek, G. Lenzini, and M. Petrocchi, Team
Automata for Security Analysis of Multicast/Broadcast Communication. In
*Proceedings of the ATPN-Workshop on Issues in Security and Petri Nets (WISP'03), Eindhoven, The Netherlands*(N. Busi, R. Gorrieri, and F. Martinelli, eds.), Beta Research School for Operations Management and Logistics, Department of Technology Management, Eindhoven University of Technology, 2003, 57 - 71.

Initiates the use of team automata for the security analysis of multicast and broadcast communication. To this aim, team automata are used to model an instance of a particular stream signature protocol, while a well-established theory for defining and verifying a variety of security properties is reformulated in terms of team automata. - [Bee03]:
M.H. ter Beek,
*Team Automata - A Formal Approach to the Modeling of Collaboration Between System Components*. Ph.D. thesis, Leiden Institute of Advanced Computer Science, Leiden University, 2003.

Studies formal aspects of team automata, focussing on the flexibility team automata offer when modeling collaboration between system components. Contains the state-of-the art of research on (using) team automata by mid 2003. - [CK04b]:
J. Carmona and J. Kleijn, Interactive Behaviour of Multi-Component Systems.
In
*Proceedings of the Workshop on Token-Based Computing (ToBaCo'04) - Affiliated to ICATPN'04, Bologna, Italy*(J. Cortadella and A. Yakovlev, eds.), Università di Bologna, 2004, 27 - 31.

This extended abstract discusses a preliminary proposal for a robust enough notion to guarantee correct (interactive) behaviour of systems (team automata) consisting of an arbitrary number of components and which may be constructed iteratively. - [BLP05]:
M.H. ter Beek, G. Lenzini, and M. Petrocchi, Team
Automata for Security - A Survey -. In
*Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages, and Systems (SecCo'04), London, UK*(R. Focardi and G. Zavattaro, eds.),*Electronic Notes in Theoretical Computer Science*128, 5, Elsevier Science Publishers, 2005, 105 - 119.

Presents a survey of the use of team automata for the specification and analysis of some issues from the field of security. - [EP04b]:
L. Egidi and M. Petrocchi, Modelling a Secure Agent with Team Automata. In
*Proceedings of the 1st International Workshop on Views On Designing Complex Architectures (VODCA'04), Bertinoro, Italy*(M.H. ter Beek and F. Gadducci, eds.),*Electronic Notes in Theoretical Computer Science*142, Elsevier Science Publishers, 2006, 111 - 127

Team automata are used to model and verify a protocol for securing agents in a hostile environment, focusing on privacy properties of the agents. This is the first attempt to use team automata for the analysis of privacy properties. - [BK05]:
M.H. ter Beek and J. Kleijn, Modularity for Teams of
I/O Automata.
*Information Processing Letters*95, 5 (2005), 487 - 495.

Shows how Input/Output automata fit in the framework of team automata, thus making it possible to view certain notions and results regarding their modular structure as special instances of more general observations. - [Pet05]:
M. Petrocchi,
*Aspects of Modeling and Verifying Secure Procedures*. Ph.D. thesis, Dipartimento di Ingegneria dell'Informazione, Università di Pisa, 2005.

Chapter 4:*The Team Automata Chapter*of this Ph.D. thesis is devoted to modeling and analysis in the framework of team automata. A first part describes a relevant multicast security protocol and a secure protocol for mobile agents, by means of team automata. New analysis strategies within team automata are then presented. Finally, the modeled protocols are analyzed by means of the above-cited strategies. - [Len05]:
G. Lenzini,
*Integration of Analysis Techniques in Security and Fault-Tolerance*. Ph.D. thesis, Centre for Telematics and Information Technology, University of Twente, CTIT Ph.D. Thesis Series No. 05-70, 2005.

Chapter 6:*Security Analysis with Team Automata*of this Ph.D. thesis describes how to model an insecure scenario for cryptographic multicast/broadcast protocols in terms of team automata and it proposes also the definition of GNDC theory for team automata. Moreover it shows how, once established the GNDC framework in terms of team automata, it is possible to reuse part of the analysis theory developed for process algebra in the automata world so that integrity properties can be proved. - [BLP06]:
M.H. ter Beek, G. Lenzini, and M. Petrocchi, A Team Automaton Scenario for the Analysis of Security Properties in Communication
Protocols.
*Journal of Automata, Languages and Combinatorics*11, 4 (2006), 345 - 374.

Shows that team automata are well suited for the analysis of security aspects in communication protocols. To this aim, an insecure communication scenario for team automata - general enough to encompass various communication protocols - is defined and the Generalized Non-Deducibility on Compositions schema - originally introduced in the context of process algebrae - is reformulated in terms of team automata. Based on the resulting team automata framework, two analysis strategies that can be used to verify security properties of communication protocols are developed. Two case studies show how this framework can be used. - [SSM07]:
M. Sharafi, F. Shams Aliee, and A. Movaghar, A Review on Specifying
Software Architectures Using Extended Automata-Based Models. In
*Proceedings of the International Symposium on Fundamentals of Software Engineering (FSEN'07), Tehran, Iran*(F. Arbab and M. Sirjani, eds.),*Lecture Notes in Computer Science*4767, Springer-Verlag, Berlin, 2007, 423 - 431.

Compares and evaluates three automata-based models (I/O automata, interface automata and team automata) and their abilities to model different aspects of components interaction in software architectures. Opts for team automata and uses them as a middleware to formally specify well-known architectural descriptions in UML2.0. A Limitation of most current automata-based models, so-called "actions interleaving", is also discussed and some approaches to overcome this limitation are described. - [BGJ08]:
M.H. ter Beek, F. Gadducci, and D. Janssens, A
Calculus for Team Automata. In
*Proceedings of the Brazilian Symposium on Formal Methods (SBMF'06), Natal, Rio Grande do Norte, Brazil*(A. Martins Moreira and L. Ribeiro, eds.),*Electronic Notes in Theoretical Computer Science*195, Elsevier Science Publishers, 2008, 41 - 55.

A process calculus for modelling team automata is introduced, extending some classical results on I/O automata. As a side result, the family of team automata that guarantees a degree of compositionality is widened slightly. - [Sha08]:
M. Sharafi, Extending Team Automata to Evaluate Software Architectural Design. In
*Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'08), Turku, Finland*, IEEE Computer Society, 2008, 393 - 400.

Describes the benefits of Team Automata over similar automata models and shows how to extend them to specify and evaluate performance of components interaction in Software Architectures. Also presents an application system example of using the introduced approach. - [BK09]:
M.H. ter Beek and J. Kleijn, Associativity of Infinite Synchronized Shuffles and Team Automata.
*Fundamenta Informaticae*91, 3-4 (2009), 437 - 461.

Motivated by basic methods to compose team automata, investigates the associativity of different (potentially unfair) synchronized shuffle operations. Proves that for the synchronized shuffle operations under consideration, a natural notion of associativity exists, also in case of unfairness. Applies these associativity results to show that certain team automata are compositional by relating the various synchronization mechanisms for team automata to corresponding shuffle operations. - [JVK10]:
N. Jaisankar, S. Veeramalai, and A. Kannan, Team Automata Based Framework
for Spatio-Temporal RBAC Model. In
*Information Processing and Management - Proceedings of the International Conference on Recent Trends in Business Administration and Information Processing (BAIP'10), Trivandrum, Kerala, India*(V.V. Das*et al.*, eds.),*Communications in Computer and Information Science*70, Springer-Verlag, Berlin, 2010, 586 - 591.

Known access control strategies are given a formal description in terms of synchronization in Team Automata. - [BK12]:
M.H. ter Beek and J. Kleijn, Vector Team Automata.
*Theoretical Computer Science*429 (2012), 21 - 29.

Vector team automata are team automata with an explicit representation of synchronizations. This makes a translation possible of a subclass of vector team automata into individual token net controllers, a model of labeled Petri nets developed within the framework of vector controlled concurrent systems. - [CK13]:
J. Carmona and J. Kleijn, Compatibility in a multi-component environment.
*Theoretical Computer Science*484 (2013), 1 - 15.

A generalized notion of I/O compatibility in the context of the team automata framework is presented. Consequently the question of how to define correct interaction (compatibility) in a multi-component environment and how to deal with synchronization strategies different from the synchronous product is addressed. - [BK14]:
M.H. ter Beek and J. Kleijn, On Distributed Cooperation and Synchronised Collaboration.
*Journal of Automata, Languages and Combinatorics*19, 1-4 (2014), 17 - 32.

Investigates how to transfer the team automata concept of collaboration by synchronizing shared actions to grammars by defining grammar teams that agree on the generation of shared terminal symbols based on a novel notion of competence. The idea is first illustrated for the case of regular grammars and then for the case of context-free grammars. - [BCK16]:
M.H. ter Beek, J. Carmona, and J. Kleijn, Conditions for Compatibility of Components: The Case of Masters and Slaves. In
*Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16), Corfu, Greece*(T. Margaria and B. Steffen, eds.),*Lecture Notes in Computer Science*9952, Springer, Berlin, 2016, 784 - 805.

In search for precise conditions for the compatibility of components in systems of systems that (by construction) guarantee correct communications, free from message loss and deadlocks, a definition of compatibility for components that applies to any synchronisation policy allowed by team automata is proposed, after which its application to master-slave synchronisations is briefly discussed.

Modeling a system as a team automaton in the early phases of design forces one to identify the active components of the system and to consider the intended communications and synchronizations in detail, which is bound to lead to a better understanding of system functionality and to explicit and unambiguous design choices. This forms the basis of further design and implementation, while at the same time the mathematically rigorous definitions provide the possibility of formal analysis tools for proving crucial design properties, without first having to implement the design.

Consequently, for each external action separately, a decision is made as to how and when the components should synchronize on this action. If the action is supposed to be a passive action that may not be under the component's local control, then it can be designated as an input action of that component, otherwise as an output action. If such a distinction between the roles of an external action is not necessary, then the choice is arbitrary. A natural option would be to make it an output action in all components in which it occurs. Once the synchronization constraints for each external action have been determined, one may apply, e.g., a maximality principle to construct a unique team automaton satisfying all constraints.

The team automata framework thus supports component-based system design by making explicit the role of actions and the choice of transitions that govern the collaboration between components. The crucial feature is the freedom of choice for the synchronizations collected in the transition relation of a team automaton. This is indeed one of the main reasons given in [Ell97] for introducing team automata to model groupware systems rather than using I/O automata for that purpose. Another important reason is that, in order for a team automaton to be capable of modeling various types of collaboration between its components by synchronizations of common actions, synchronizations between output actions of its components should not be excluded a priori. As a matter of fact, the peer-to-peer types of synchronization explicitly use the possibility to synchronize on output actions. Finally, no matter how convenient input enabling may be when modeling reactive systems, it does hinder a realistic modeling of collaborations that involve humans - in fact, Tuttle himself was the first to acknowledge this when he introduced I/O automata - while modeling such collaborations was one of the main reasons for the introduction of team automata.

This site is administered by Maurice ter Beek.