Efficiency of automata in semi-commutation verification techniques

International audience; Computing the image of a regular language by the transitive closure of a relation is a central question in Regular Model Checking. In a recent paper Bouajjani, Muscholl and Touili \cite{Anca} proved that the class of regular languages L -- called APC -- of the form of a union of L{0,j}L{1,j}L{2,j}... L{k_j,j}$, where the union is finite and each L{i,j} is either a single symbol or a language of the form B* with B a subset of the alphabet, is closed under all semi-commutation relations R. Moreover a recursive algorithm on the regular expressions was given to compute R*(L). This paper provides a new approach, based on automata, for the same problem. Our approach produces a simpler and more efficient algorithm which furthermore works for a larger class of regular languages closed under union, intersection, semi-commutation relations and conjugacy. The existence of this new class, PolC, answers the open question proposed in the paper of Bouajjani and al.