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.
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.
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.