Efficiency of automata in semi-commutation verification techniques

LIFC, CNRS FRE 2661, Projet INRIA-CASSIS, Université de Franche-Comté, 16 route de Gray, 25030 Besancon Cedex, France; Gerard.Cece@univ-fcomte.fr; Pierre-Cyrille.Heam@univ-fcomte.fr; Yann.Mainier@univ-fcomte.fr

Received: 27 April 2004
Accepted: 5 December 2005

Abstract

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 UjL_0,jL_1,jL_2,j...L_kj,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 et al.