A Calculus for Team Automata
Ter Beek M. H., Gadducci F., Janssens D.
Computer Science(all) Semantics of Programming Languages. Process models Computer. Automation Theoretical Computer Science Team automata General Computer Science Compositional specification F.1.1 Models of Computation. Automata F.3.2 Models of Computation. Relations between models Semantics of Programming Languages. Algebraic approaches to semantics Process calculi Process calculus
Team automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patterns among systems, thus extending I/O automata. Furthermore, for some patterns the language recognized by a team automaton can be specified via those languages recognized by its components. We introduce a process calculus tailored over team automata. Each automaton is described by a process, such that its associated (fragment of a) labeled transition system is bisimilar to the original automaton. The mapping is moreover denotational, since the operators defined on processes are in a bijective correspondence with a chosen family of coordination patterns and that correspondence is preserved by the mapping. We thus extend to team automata a few classical results on I/O automata and their representation by process calculi. Moreover, besides providing a language for expressing team automata, we widen the family of coordination patterns for which an equational characterization of the language associated to a composite automaton can be provided. The latter result is obtained by providing a set of axioms, in ACP-style, for capturing bisimilarity in our calculus.
Source: Brazilian Symposium on Formal Methods (SBMF'06), pp. 41–55, Natal, Rio Grande do Norte, Brazil, 17-23 Settembre 2006
[2] ter Beek, M. H., “Team Automata-A Formal Approach to the Modeling of Collaboration Between System Components,” Ph.D. thesis, Leiden University (2003).
[3] ter Beek, M. H., C. A. Ellis, J. Kleijn and G. Rozenberg, Synchronizations in team automata for groupware systems, Computer Supported Cooperative Work 12 (2003), pp. 21-69.
[4] ter Beek, M. H. and J. Kleijn, Team automata satisfying compositionality, in: K. Araki, S. Gnesi and D. Mandrioli, editors, International Symposium of Formal Methods Europe, Lect. Notes in Comp. Sci. 2805 (2003), pp. 381-400.
[5] ter Beek, M. H. and J. Kleijn, Modularity for teams of I/O automata, Information Processing Letters 95 (2005), pp. 487-495.
[6] ter Beek, M. H., G. Lenzini and M. Petrocchi, Team automata for security: A survey, in: F. R. and G. Zavattaro, editors, International Workshop on Security Issues in Coordination Models, Languages, and Systems, Electr. Notes in Theor. Comp. Sci. 128 (2005), pp. 105-119.
[7] ter Beek, M. H., G. Lenzini and M. Petrocchi, A team automaton scenario for the analysis of security properties of communication protocols, Journal of Automata, Languages and Combinatorics (2006), to appear.
[8] Bergstra, J. A. and J. W. Klop, Process Algebra for Synchronous Communication, Information and Control 60 (1984), pp. 109-137.
[9] Bol, R. N. and J. F. Groote, The meaning of negative premises in transition system specifications, Journal of the ACM 43 (1996), pp. 863-914.
[10] De Nicola, R. and R. Segala, A process algebraic view of input/output automata, Theoretical Computer Science 138 (1995), pp. 391-423.
[11] Ellis, C. A., Team automata for groupware systems, in: International Conference on Supporting Group Work (1997), pp. 415-424.
[12] Hoare, C. A. R., “Communicating Sequential Processes,” Prentice Hall, 1985.
[13] Jonsson, B., Compositional specification and verification of distributed systems, ACM Transactions on Programming Languages and Systems 16 (1994), pp. 259-303.
[14] Kleijn, J., Team automata for CSCW: A survey, in: Petri Net Technology for Communication-Based Systems, Lect. Notes in Comp. Sci. 2472, Springer, 2003 pp. 295-320.
[15] Lynch, N. A., “Distributed Algorithms,” Morgan Kaufmann, 1996.
[16] Lynch, N. A. and M. R. Tuttle, An introduction to input/output automata, CWI Quarterly 2 (1989), pp. 219-246.
[17] Milner, R., “A Calculus of Communicating Systems,” Lect. Notes in Comp. Sci. 92, Springer, 1980.
[18] Plotkin, G., A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University (1981).
[19] Stark, E. W., R. Cleaveland and S. A. Smolka, A process-algebraic language for probabilistic I/O automata, in: R. Amadio and D. Lugiez, editors, International Conference on Concurrency Theory, Lect. Notes in Comp. Sci. 2761 (2003), pp. 193-207.
[20] Vaandrager, F. W., On the relationship between process algebra and input/output automata (extended abstract), in: Symposium on Logic in Computer Science (1991), pp. 387-398.
Metrics
Back to previous page
@inproceedings{oai:it.cnr:prodotti:91810,
title = {A Calculus for Team Automata},
author = {Ter Beek M. H. and Gadducci F. and Janssens D.},
doi = {10.1016/j.entcs.2007.08.022},
booktitle = {Brazilian Symposium on Formal Methods (SBMF'06), pp. 41–55, Natal, Rio Grande do Norte, Brazil, 17-23 Settembre 2006},
year = {2008}
}
0000-0002-2930-6367