HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Efficiency of Automata in Semi-Commutation Verification Techniques

Gérard Cécé 1 Pierre-Cyrille Héam 1 Yann Mainier 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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, Muscholl and Touili proved that the class of APC regular languages is closed under all semi-commutation relations R. Moreover a recursive algorithm on the regular expression is given to compute the image of an APC language by the transitive closure of R. This paper provides a new approach, based on automata, of the same question. 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, answered the open question proposed in Bouajjani and al.'s paper.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, May 29, 2006 - 11:57:56 AM
Last modification on : Friday, January 21, 2022 - 3:09:05 AM
Long-term archiving on: : Monday, April 5, 2010 - 9:33:08 PM


  • HAL Id : inria-00077039, version 1


Gérard Cécé, Pierre-Cyrille Héam, Yann Mainier. Efficiency of Automata in Semi-Commutation Verification Techniques. [Research Report] RR-5001, INRIA. 2003, pp.20. ⟨inria-00077039⟩



Record views


Files downloads