Efficiency of automata in semi-commutation verification techniques
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) no. 2, pp. 197-215.

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 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 * (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.

DOI : 10.1051/ita:2007029
Classification : 68N30
Mots-clés : regular model checking, verification, parametric systems, semi-commutations
@article{ITA_2008__42_2_197_0,
     author = {C\'ec\'e, G\'erard and H\'eam, Pierre-Cyrille and Mainier, Yann},
     title = {Efficiency of automata in semi-commutation verification techniques},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {197--215},
     publisher = {EDP-Sciences},
     volume = {42},
     number = {2},
     year = {2008},
     doi = {10.1051/ita:2007029},
     mrnumber = {2401258},
     zbl = {1144.68039},
     language = {en},
     url = {http://archive.numdam.org/articles/10.1051/ita:2007029/}
}
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 - Informatique Théorique et Applications
PY  - 2008
SP  - 197
EP  - 215
VL  - 42
IS  - 2
PB  - EDP-Sciences
UR  - http://archive.numdam.org/articles/10.1051/ita:2007029/
DO  - 10.1051/ita:2007029
LA  - en
ID  - ITA_2008__42_2_197_0
ER  - 
%0 Journal Article
%A Cécé, Gérard
%A Héam, Pierre-Cyrille
%A Mainier, Yann
%T Efficiency of automata in semi-commutation verification techniques
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2008
%P 197-215
%V 42
%N 2
%I EDP-Sciences
%U http://archive.numdam.org/articles/10.1051/ita:2007029/
%R 10.1051/ita:2007029
%G en
%F ITA_2008__42_2_197_0
Cécé, Gérard; Héam, Pierre-Cyrille; Mainier, Yann. Efficiency of automata in semi-commutation verification techniques. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) no. 2, pp. 197-215. doi : 10.1051/ita:2007029. http://archive.numdam.org/articles/10.1051/ita:2007029/

[1] 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. | MR

[2] 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.

[3] 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. | MR

[4] J. Berstel, Transductions and Context-Free Languages. B.G. Teubner, Stuttgart (1979). | MR | Zbl

[5] B. Boigelot and P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs 1102 (1996) 1-12.

[6] B. Boigelot and P. Wolper, Verifying systems with infinite but regular state spaces. In CAV'98. Lect. Notes Comput. Sci. 1427 (1998) 88-97. | MR

[7] A. Bouajjani, A. Muscholl and T. Touili, Permutation rewriting and algorithmic verification, in LICS'01. IEEE Comput. Soc. (2001) 399-408.

[8] J.A. Brzozowski, Hierarchies of aperiodic languages, 10 (1976) 33-49. | Numdam | MR | Zbl

[9] J.A. Brzozowski and I. Simon, Characterizations of locally testable languages. 4 (1973) 243-271. | MR | Zbl

[10] 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).

[11] 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). | MR

[12] V. Diekert and G. Rozenberg, Ed. Book of Traces. World Scientific, Singapore (1995). | MR

[13] Z. Esik and I. Simon, Modeling literal morphisms by shuffle. Semigroup Forum 56 (1998) 225-227. | MR | Zbl

[14] P. Godefroid and P. Wolper, A partial approach to model checking. Inform. Comput. 110 (1994) 305-326. | MR | Zbl

[15] A. Cano Gomez and J.-E. Pin, On a conjecture of schnoebelen, in DLT'03. (2003). | Zbl

[16] A. Cano Gomez and J.-E. Pin, Shuffle on positive varieties of languages. 312 (2004) 433-461. | MR | Zbl

[17] G. Guaiana, A. Restivo and S. Salemi, On the trace product and some families of languages closed under partial commutations. 9 (2004) 61-79. | MR | Zbl

[18] P.-C. Héam, Some complexity results for polynomial rational expressions. 299 (2003). | MR | Zbl

[19] J. Hopcroft and J. Ullman, Introduction to automata theory, languages, and computation. Addison-Wesley (1980). | MR | Zbl

[20] X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system, release 3.06. Inria, 2002.

[21] D. Lugiez and Ph. Schnoebelen, The regular viewpoint on pa-processes, in 9th Int. Conf. Concurrency Theory (CONCUR'98). . 1466 (1998). | MR | Zbl

[22] J.-F. Perrot, Variété de langages et opérations. 7 (1978) 197-210. | MR | Zbl

[23] J.-E. Pin, Varieties of formal languages. Foundations of Computer Science (1984). | MR | Zbl

[24] J.-E. Pin and P. Weil, Polynomial closure and unambiguous product. Theor. Comput. Syst. 30 (1997) 1-39. | MR | Zbl

[25] Ph. Schnoeboelen, Decomposable regular languages and the shuffle operator. EATCS Bull. 67 (1999) 283-289.

[26] H. Straubing, Finite semigroups varieties of the form V*D. 36 (1985) 53-94. | MR | Zbl

[27] P. Tesson and D. Thérien, Diamonds are forever: the variety da, in International Conference on Semigroups, Algorithms, Automata and Languages (2002). | MR | Zbl

[28] W. Thomas, Classifying regular events in symbolic logic. 25 (1982) 360-375. | MR | Zbl

[29] D. Thérien, Classification of finite monoids: the language approach. 14 (1981) 195-208. | MR | Zbl

[30] T. Touili. Regular model checking using widening techniques, in 1st Vepas Workshop, volume 50 of Electronic Notes in TCS (2001).

Cité par Sources :