# Efficiency of automata in semi-commutation verification techniques

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

RAIRO - Theoretical Informatics and Applications (2007)

- Volume: 42, Issue: 2, page 197-215
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topCécé, Gérard, Héam, Pierre-Cyrille, and Mainier, Yann. "Efficiency of automata in semi-commutation verification techniques." RAIRO - Theoretical Informatics and Applications 42.2 (2007): 197-215. <http://eudml.org/doc/92867>.

@article{Cécé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 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.
},

author = {Cécé, Gérard, Héam, Pierre-Cyrille, Mainier, Yann},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Regular model checking; verification; parametric systems; semi-commutations; image of a regular language; transitive closure; model checking},

language = {eng},

month = {9},

number = {2},

pages = {197-215},

publisher = {EDP Sciences},

title = {Efficiency of automata in semi-commutation verification techniques},

url = {http://eudml.org/doc/92867},

volume = {42},

year = {2007},

}

TY - JOUR

AU - Cécé, Gérard

AU - Héam, Pierre-Cyrille

AU - Mainier, Yann

TI - Efficiency of automata in semi-commutation verification techniques

JO - RAIRO - Theoretical Informatics and Applications

DA - 2007/9//

PB - EDP Sciences

VL - 42

IS - 2

SP - 197

EP - 215

AB -
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.

LA - eng

KW - Regular model checking; verification; parametric systems; semi-commutations; image of a regular language; transitive closure; model checking

UR - http://eudml.org/doc/92867

ER -

## References

top- P.A. Abdulla, A. Bouajjani and B. Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, in CAV'98. Lect. Notes Comput. Sci.1427 (1998) 305–322.
- P. Abdulla, A. Annichini and A. Bouajjani, Algorithmic verification of lossy channel systems: An appliction to the bounded retransmission protocol, in TACAS'99. Lect. Notes Comput. Sci.1579 (1999) 208–222.
- P.A. Abdulla, B. Jonsson, M. Nilsson and J. d'Orso, Algorithmic improvements in regular model checking, in CAV'03. Lect. Notes Comput. Sci.2725 (2003) 236–248. Zbl1278.68150
- J. Berstel, Transductions and Context-Free Languages. B.G. Teubner, Stuttgart (1979).
- B. Boigelot and P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, in Proc. of 8th CAV (August), USA1102 (1996) 1–12.
- B. Boigelot and P. Wolper, Verifying systems with infinite but regular state spaces. In CAV'98. Lect. Notes Comput. Sci.1427 (1998) 88–97.
- A. Bouajjani, A. Muscholl and T. Touili, Permutation rewriting and algorithmic verification, in LICS'01. IEEE Comput. Soc. (2001) 399–408. Zbl1107.68052
- J.A. Brzozowski, Hierarchies of aperiodic languages, 10 (1976) 33–49.
- J.A. Brzozowski and I. Simon, Characterizations of locally testable languages. 4 (1973) 243–271. Zbl0255.94032
- G. Cécé, P.-C. Héam and Y. Mainier, Clôture transitives de semi-commutations et model-checking régulier, in AFADL'04 (2004).
- V. Diekert and Y. Métivier, Partial commutation and traces, in Handbook on Formal Languages, volume III, edited by G. Rozenberg and A. Salomaa, Springer, Berlin-Heidelberg-New York (1997).
- V. Diekert and G. Rozenberg, Ed. Book of Traces. World Scientific, Singapore (1995).
- Z. Esik and I. Simon, Modeling literal morphisms by shuffle. Semigroup Forum56 (1998) 225–227. Zbl0982.20056
- P. Godefroid and P. Wolper, A partial approach to model checking. Inform. Comput.110 (1994) 305–326. Zbl0806.68079
- A. Cano Gomez and J.-E. Pin, On a conjecture of schnoebelen, in DLT'03. (2003). Zbl1037.68075
- A. Cano Gomez and J.-E. Pin, Shuffle on positive varieties of languages. 312 (2004) 433–461. Zbl1143.68431
- G. Guaiana, A. Restivo and S. Salemi, On the trace product and some families of languages closed under partial commutations. 9 (2004) 61–79. Zbl1102.68065
- P.-C. Héam, Some complexity results for polynomial rational expressions. 299 (2003). Zbl1042.68063
- J. Hopcroft and J. Ullman, Introduction to automata theory, languages, and computation. Addison-Wesley (1980). Zbl0847.68065
- X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system, release 3.06. Inria, 2002.
- D. Lugiez and Ph. Schnoebelen, The regular viewpoint on pa-processes, in 9th Int. Conf. Concurrency Theory (CONCUR'98). . 1466 (1998). Zbl0932.68052
- J.-F. Perrot, Variété de langages et opérations. 7 (1978) 197–210. Zbl0398.68035
- J.-E. Pin, Varieties of formal languages. Foundations of Computer Science (1984).
- J.-E. Pin and P. Weil, Polynomial closure and unambiguous product. Theor. Comput. Syst.30 (1997) 1–39. Zbl0872.68119
- Ph. Schnoeboelen, Decomposable regular languages and the shuffle operator. EATCS Bull.67 (1999) 283–289.
- H. Straubing, Finite semigroups varieties of the form V*D. 36 (1985) 53–94. Zbl0561.20042
- P. Tesson and D. Thérien, Diamonds are forever: the variety da, in International Conference on Semigroups, Algorithms, Automata and Languages (2002). Zbl1031.20049
- W. Thomas, Classifying regular events in symbolic logic. 25 (1982) 360–375. Zbl0503.68055
- D. Thérien, Classification of finite monoids: the language approach. 14 (1981) 195–208. Zbl0471.20055
- T. Touili. Regular model checking using widening techniques, in 1st Vepas Workshop, volume 50 of Electronic Notes in TCS (2001). Zbl1262.68130

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.