P. Abdulla, A. Annichini, and A. Bouajjani, Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol, TACAS'99, pp.208-222, 1999.
DOI : 10.1007/3-540-49059-0_15

A. [. Abdulla, B. Bouajjani, and . Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, CAV'98, pp.305-322, 1998.
DOI : 10.1007/BFb0028754

P. Aziz-abdulla, B. Jonsson, M. Nilsson, and J. Orso, Algorithmic Improvements in Regular Model Checking, CAV'03, 2003.
DOI : 10.1007/978-3-540-45069-6_25

]. M. Arf91 and . Arfi, Opération polynomiales et hiérarchies de concaténation, Theoretical Computer Science, vol.91, pp.71-84, 1991.

L. [. Berstel and . Boasson, Shuffle factorization is unique, Theoretical Computer Science, vol.273, issue.1-2, 1999.
DOI : 10.1016/S0304-3975(00)00433-3
URL : https://hal.archives-ouvertes.fr/hal-00619363

J. Berstel, L. Boasson, O. Carton, B. Petazzoni, and J. Pin, Operations preserving regular languages, Theoretical Computer Science, vol.354, issue.3, pp.405-420, 2006.
DOI : 10.1016/j.tcs.2005.11.034

J. Berstel, Transductions and Context-Free Languages, B.G. Teubner, 1979.
DOI : 10.1007/978-3-663-09367-1
URL : https://hal.archives-ouvertes.fr/hal-00619779

P. [. Boigelot and . Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, Proc. of 8 th CAV, pp.1-12, 1996.
DOI : 10.1007/3-540-61474-5_53

A. [. Bouajjani, T. Muscholl, and . Touili, Permutation rewriting and algorithmic verification, LICS'01, pp.399-408, 2001.
URL : https://hal.archives-ouvertes.fr/hal-00161120

A. Bouajjani, A. Muscholl, and T. Touili, Permutation rewriting and algorithmic verification, Information and Computation, vol.205, issue.2, pp.199-224, 2007.
DOI : 10.1016/j.ic.2005.11.007
URL : https://hal.archives-ouvertes.fr/hal-00161120

]. J. Brz76 and . Brzozowski, Hierarchies of aperiodic languages, Informatique théorique et Application/Theoretical Informatics and Applications, pp.33-49, 1976.

I. [. Brzozowski and . Simon, Characterizations of locally testable events, Discrete Mathematics, vol.4, issue.3, pp.243-271, 1973.
DOI : 10.1016/S0012-365X(73)80005-6

[. Boigelot and P. Wolper, Verifying systems with infinite but regular state spaces, CAV'98, pp.88-97, 1998.

G. Cécé, P. Héam, and Y. Mainier, Efficiency of automata in semi-commutation verification techniques, 2003.

. [. Héam, V. Diekert, and . Métivier, Partial Commutation on Traces, volume III of Handbook on Formal Languages, 1997.

I. [. Esik and . Simon, Modeling Literal Morphisms by Shuffle, Semigroup Forum, vol.56, issue.2, pp.225-227, 1998.
DOI : 10.1007/PL00005943

B. Genest and A. Muscholl, Message Sequence Charts: A Survey, Fifth International Conference on Application of Concurrency to System Design (ACSD'05), pp.2-4, 2005.
DOI : 10.1109/ACSD.2005.25

[. Gomez and J. Pin, On a Conjecture of Schnoebelen, DLT'03, pp.35-54, 2003.
DOI : 10.1007/3-540-45007-6_4
URL : https://hal.archives-ouvertes.fr/hal-00112692

[. Gomez and J. Pin, Shuffle on positive varieties of languages, Theoretical Computer Science, vol.312, issue.2-3, 2004.
DOI : 10.1016/j.tcs.2003.10.034
URL : https://hal.archives-ouvertes.fr/hal-00112826

J. [. Hopcroft and . Ullman, Introduction to automata theory, languages, and computation, 1980.
DOI : 10.1145/568438.568455

. [. Lugiez, . Ph, and . Schnoebelen, The regular viewpoint on pa-processes, 9th Int. Conf. Concurrency Theory (CONCUR'98), volume 1466 of Lecture Notes in Computer Science, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073287

A. Muscholl and D. Peled, From Finite State Communication Protocols to High-Level Message Sequence Charts, Lecture Notes in Computer Science, vol.2076, pp.720-731, 2001.
DOI : 10.1007/3-540-48224-5_59

. Nrr-+-94-]-m, G. D. Nivat, C. Ramkumar, A. Pandu-rangan, R. Saoudi et al., Efficient parallel shuffle recognition, Parallel Processing Letters, vol.4, pp.455-463, 1994.

]. Per78 and . Perrot, Variété de langages et opérations, Theoretical Computer Science, vol.7, pp.197-210, 1978.

J. Pin, On the languages accepted by finite reversible automata, Automata, Languages and Programming, 14th International Colloquium, pp.237-249, 1987.
DOI : 10.1007/3-540-18088-5_19

]. Pin94 and . Pin, Polynomial closure of group languages and open sets of the Hall topology, Lecture Notes in Computer Science, vol.820, pp.424-432, 1994.
DOI : 10.1007/3-540-58201-0_87

B. Pradeep, C. Murthy, and S. Ram, A constant time string shuffle algorithm on reconfigurable meshes, International Journal of Computer Mathematics, vol.68, issue.3-4, pp.251-259, 1998.
DOI : 10.1109/21.17370

[. Pin and P. Weil, Polynomial closure and unambiguous product, Theory Comput. Systems, vol.30, pp.1-39, 1997.
URL : https://hal.archives-ouvertes.fr/hal-01248158

I. E. Radford, A natural ring basis for the shuffle algebra and an application to group schemes, Journal of Algebra, vol.58, issue.2, pp.432-454, 1979.
DOI : 10.1016/0021-8693(79)90171-6

]. Spe86 and . Spehner, Le calcul rapide des mélanges de deux mots, Theoretical Computer Science, vol.47, pp.181-203, 1986.

]. H. Str85 and . Straubing, Finite semigroups varieties of the form V * D, Journal of Pure and Applied Algebra, vol.36, pp.53-94, 1985.

]. W. Tho82 and . Thomas, Classifying regular events in symbolic logic, Journal of Computer and System Science, vol.25, pp.360-375, 1982.

]. D. Thé81 and . Thérien, Classification of finite monoids: the language approach, Theoretical Computer Science, vol.14, pp.195-208, 1981.

]. T. Tou01 and . Touili, Regular model checking using widening techniques, 1st Vepas Workshop, 2001.

D. [. Tesson and . Thérien, DIAMONDS ARE FOREVER: THE VARIETY DA, Semigroups, Algorithms, Automata and Languages, 2002.
DOI : 10.1142/9789812776884_0021

L. Unité-de-recherche-inria-lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès

I. Unité-de-recherche and . Rennes, IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38330 Montbonnot-St-Martin (France) Unité de recherche INRIA Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche, 2004.

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399