RAIRO-Theor. Inf. Appl.
Volume 42, Number 2, April-June 2008
|Page(s)||197 - 215|
|Published online||25 September 2007|
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;
Accepted: 5 December 2005
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.
Mathematics Subject Classification: 68N30
Key words: Regular model checking / verification / parametric systems / semi-commutations
© EDP Sciences, 2007
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.