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 et al. [IEEE Comput. Soc. (2001) 399–408] proved that the class of
regular languages L – called APC – of the form UjL0,jL1,jL2,j...Lkj,j, where the union is finite and each
Li,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 et al.