Issue RAIRO-Theor. Inf. Appl. Volume 42, Number 2, April-June 2008 Page(s) 197 - 215 DOI 10.1051/ita:2007029 Published online 25 September 2007

RAIRO-Theor. Inf. Appl. 42, 197-215 (2008)
DOI: 10.1051/ita:2007029

Efficiency of automata in semi-commutation verification techniques

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

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 April 27, 2004. Accepted December 5, 2005. Published online 25 September 2007.)

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 L_0,jL_1,jL_2,jL_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, Pol , answers the open question proposed in the paper of Bouajjani et al.

Mathematics Subject Classification. 68N30

Key words: Regular model checking -- verification -- parametric systems -- semi-commutations


© EDP Sciences 2007

What is OpenURL?