Team Automata
What are Team Automata (good for)?
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.
[This is a not so frequently updated version of the Introduction of [Bee03].]
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]).
Background
A set of interacting, interrelated, or interdependent components forming a
complex whole is what we mean by the frequently used, but seldom defined
notion of a system. The human body and computers are thus examples
of a system. A system is distributed if it consists of separate
components but nevertheless appears to its users as a single coherent system.
It does not have a single locus of control, but its components collaborate
by way of interactions. The internet is one of the best known distributed
systems.
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.
Computer Supported Cooperative Work
As the presence of computer-based systems in daily-life work situations
continues to increase, the understanding of how people work together and ways
in which computer technology can assist, has become more and more important.
This has resulted in the emergence of Computer Supported Cooperative
Work (CSCW for short) as an inherently multi-disciplinary field of
research. By the nature of the field, part of the computer technology
consists of multi-user software and hardware, called groupware.
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.
Formal Methods
Mathematical techniques tailored for the specification and verification of
systems are known as formal methods. This field of research cuts
across many areas of computer science and comes with an impressive body of
literature. A brief comparison of the main features of team automata with
some of the best-known formalisms in this field follows later on, while a
more detailed comparison with two such formalisms can be found in [Kle03] and [BK05].
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.
The Model
We now provide an overview of the team automata framework. We begin with a
brief sketch of the overall structure of team automata and subsequently we
introduce them in more detail. Analogous to [Bee03] we follow an incremental
presentation of team automata.
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.
Automata
Automata or labeled transition systems are a well-known model
underlying formal specifications of systems. An automaton consists of a set
of states, a set of actions, a set of labeled transitions between states,
and a set of initial states. Labels represent actions and a transition's
label indicates the action causing the transition from one state to another.
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.
Synchronized Automata
A synchronized automaton over a set of automata is an automaton,
determined by the way in which its constituting automata cooperate by means
of synchronized transitions. Its (initial) states are combinations - a
cartesian product - of (initial) states of its constituting automata. Its
actions are the actions of its constituting automata. Its transitions,
finally, are synchronizations of labeled transitions of its
constituting automata modeling the simultaneous execution of the same single
action by several (one or more) automata. The label of a transition is the
action being simultaneously executed. When the synchronized automaton changes
state by executing an action, all automata which participate simultaneously
change state by executing that action, while all others remain idle.
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.
Team Automata
A component automaton is an automaton in which input,
output, and internal actions are distinguished. Input
actions are not under the automaton's control, but instead are triggered by
the environment including other component automata. Output and internal
actions are under its control, but only the output actions are observable by
other automata. Input and output actions together constitute the external
actions and they form the interface between the automaton and its
environment, whereas the internal actions are not available for interactions.
This is formally achieved by requiring that the internal actions of each
component automaton involved are unique to that automaton, which naturally
prohibits synchronizations of internal actions with other automata.
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.
Team Automata Versus Other Models
Team automata are not an isolated model but have several features which bear
a close resemblance to characteristics of other models from the literature.
We now discuss three such features in general terms.
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.
Conclusion
Team automata thus form a formal framework for component-based system design.
They are based on the well-known method for modeling collaboration between
system components by synchronizations of actions or transitions. A
distinguishing feature of team automata is the freedom to choose on which
actions and when their constituting component automata synchronize. In
addition, there is the distinction of a team automaton's alphabet into input,
output, and internal actions.
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.
See the
Bibliography
of Team Automata (also available in
BibTeX or
pdf format)
for all publications on Team Automata.
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.
- [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.
- [BCHK17]:
M.H. ter Beek, J. Carmona, R. Hennicker, and J. Kleijn, Communication Requirements for Team Automata. In Proceedings of the 19th IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'17), Neuchâtel, Switzerland (J.-M. Jacquet and M. Massink, eds.), Lecture Notes in Computer Science 10319, Springer, Berlin, 2017, 256 - 277.
Compatibility of components is studied in the context of systems of reactive components which may communicate through the synchronised execution of common actions, modelled as team automata, without imposing any a priori restrictions on the synchronisation policy followed to combine the components. A family of representative synchronisation types based on the number of sending and receiving components participating in synchronisations is identified and a generic procedure is given to derive, for each synchronisation type, requirements for receptiveness and for responsiveness of team automata.
- [BHK20a]:
M.H. ter Beek, R. Hennicker, and J. Kleijn, Team Automata@Work: On Safe Communication. In Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'20), Valletta, Malta (S. Bliudze and L. Bocchi, eds.), Lecture Notes in Computer Science 12134, Springer, Cham, 2020, 77 - 85.
Requirements for safe communication in systems of team automata are studied. Three extensions to the concept of safe communication, in terms of reception and responsiveness requirements as originally defined for synchronisation policies determined by a synchronisation type, are proposed. First, compliance, i.e. satisfaction of communication requirements, does not have to be immediate. Second, the synchronisation type (and hence the communication requirements) no longer has to be uniform, but can be specified per action. Third, final states permit to distinguish between possible and guaranteed executions of actions.
- [BHK20b]:
M.H. ter Beek, R. Hennicker, and J. Kleijn, Compositionality of Safe Communication in Systems of Team Automata. In Proceedings of the 17th International Colloquium on Theoretical Aspects of Computing (ICTAC'20), Macau, China (V.K.I. Pun, A. Simão, and V. Stolz, eds.), Lecture Notes in Computer Science 12545, Springer, Cham, 2020, 200 - 220.
Guarantees for safe communication in systems of systems modelled as (extended) team automata is studied. Team automata are extended with synchronisation type specifications, which determine specific synchronisation policies fine-tuned for particular application domains and generate communication requirements for receptiveness and responsiveness. A new, liberal version of requirement satisfaction is proposed, which allows teams to execute arbitrary intermediate actions before being ready for the required communication. It is shown that composition of systems behaves well with respect to synchronisation type specifications, by providing criteria that ensure the preservation of local communication properties when (extended) team automata are composed.
- [BCHP21]:
M.H. ter Beek, G. Cledou, R. Hennicker, and J. Proença, Featured Team Automata. In Proceedings of the 24th International Symposium on Formal Methods (FM'21), Beijing, China (M. Huisman, C. Păsăreanu, and N. Zhan, eds.), Lecture Notes in Computer Science 13047, Springer, Cham, 2021, 483 - 502.
Featured team automata are proposed to support variability in the development and analysis of teams. A featured team automaton concisely describes a family of concrete product models for specific configurations determined by feature selection. The focus is on the analysis of communication-safety properties, but doing so product-wise quickly becomes impractical. Therefore, it is investigated how to lift notions of receptiveness (no message loss) to the level of family models. It is shown that featured (weak) receptiveness of featured team automata characterises (weak) receptiveness for all product instantiations. A prototypical tool supports the developed theory.
- [BCHP23]:
M.H. ter Beek, G. Cledou, R. Hennicker, and J. Proença, Can we Communicate? Using Dynamic Logic to Verify Team Automata. In Proceedings of the 25th International Symposium on Formal Methods (FM'23), Lübeck, Germany (M. Chechik, J.-P. Katoen, and M. Leucker, eds.), Lecture Notes in Computer Science 14000, Springer, Cham, 2023, 122 - 141.
Given a team automaton, one can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied). Previous work focused on how to identify these communication properties. However, verifying automatically these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototypical tool supports the developed theory, using an encoding to interact with the mCRL2 toolset for model checking.
- [BHP23]:
M.H. ter Beek, R. Hennicker, and J. Proença, Realisability of Global Models of Interaction. In Proceedings of the 20th International Colloquium on Theoretical Aspects of Computing (ICTAC'23), Lima, Peru (E. Ábrahám, C. Dubslaff and S. L. Tapia Tarifa, eds.), Lecture Notes in Computer Science 14446, Springer, Cham, 2023, 236 - 255.
This paper considers global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems - one per agent - which are executed concurrently using synchronous communication. The core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. The authors identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence, after which they investigate, for both variants, realisability conditions to be checked on global models. Finally, they propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. This paper is accompanied by a tool that implements realisability checks and synthesises realisations.
- [Pro23]:
J. Proença, Overview on Constrained Multiparty Synchronisation in Team Automata. In Revised Selected Papers of the 19th International Conference on Formal Aspects of Component Software (FACS'23) (J. Cámara and S.-S. Jongmans, eds.), Lecture Notes in Computer Science 14485, Springer, Cham, 2023, 194 - 205.
This paper provides an overview on recent work on Team Automata and revisits the team automata notion of synchronisation in other well-known concurrency models, such as Reo, BIP, Choreography Automata, and Multiparty Session Types. The author also addresses realisability of Team Automata, i.e., how to infer a network of interacting automata from a global specification, taking into account that this realisation should satisfy exactly the same properties as the global specification, proposing a set of interesting directions of challenges and future work in the context of Team Automata or similar concurrency models.
- [BHP24]:
M.H. ter Beek, R. Hennicker, and J. Proença, Team Automata: Overview and Roadmap. In Proceedings of the 26th IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'24), Groningen, The Netherlands (I. Castellani and F. Tiezzi, eds.), Lecture Notes in Computer Science , Springer, Cham, 2024.
In this paper, the specific notion of synchronisation and composition of team automata is revisited and related to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types.
The authors then identify several aspects that have recently been investigated for team automata and related models.
These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?) and tool support (what has been automatised or implemented?).
This presentation provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.
Before giving an impression of how - in theory - team automata can be used for
system design and where - in practice - they have actually been used, note
that there is a list of people using Team Automata.
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.
In Theory
To model a system as a team automaton, first the components have to be
identified. Each of them should be given a description in the form of an
automaton - an easy to understand model that moreover forms the basis for
system descriptions in a number of model-checking tools (such as, e.g.,
Spin). Based on the idea of
synchronizations of common actions, these components can be connected in
order to collaborate. Within each component, a distinction has to be made
between internal actions - which are not available for synchronization with
other components - and external actions - which can be used to synchronize
components and may be subject to synchronization restrictions. By assigning
such different roles to actions it is possible to describe many types of
collaboration.
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.
In Practice
An increasing number of papers bears witness to the usefulness of team
automata in the early design phase of reactive systems in general, and of
groupware systems in particular. Moreover, these examples are not limited
to modeling within CSCW (see, e.g., [Ell97], [BEKR01a], [BEKR01b], and
[BB03]) but extend to areas such as software engineering (see, e.g., [HB00],
[EG02], and [SSM07]) and - most recently - security (see, e.g., [BLP03],
[BLP05], [BLP06], and [EP06]). In fact, a spectrum from hardware components
to protocols for interacting groups of people has been modeled by team automata.
There is still quite some work left to do, though. For one, the components of a
team currently cannot exchange any information, i.e. they have no private memory.
In order to be useful also in later stages of the design of groupware systems
(or to model, e.g., workflow systems) team automata should thus - among other
things - be extended with the flow of information between components. An initial
attempt in this direction was undertaken in [BCM03]. Furthermore, team automata
are currently inappropriate for capturing aspects of group activity such as
social aspects and informal unstructured activity.
This site is administered by
Maurice ter Beek.
