Efficiency of automata in semi-commutation verification techniques

Cécé, Gérard  ; Héam, Pierre-Cyrille  ; Mainier, Yann

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) no. 2, pp. 197-215

Résumé

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 ${\cup }_j$$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^{*}\left(L\right)$. 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, Pol$𝒞$, answers the open question proposed in the paper of Bouajjani et al.

Détail

DOI : 10.1051/ita:2007029

Classification : 68N30
Keywords: regular model checking, verification, parametric systems, semi-commutations