Efficiency of automata in semi-commutation verification techniques

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

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2008)

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

Abstract

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

How to cite

top

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

@article{Cécé2008,
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 $\cup _j$$L_\{0,j\}$$L_\{1,j\}$$L_\{2,j\}$$\ldots $$ 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$\mathcal \{C\}$, 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 - Informatique Théorique et Applications},
keywords = {regular model checking; verification; parametric systems; semi-commutations; image of a regular language; transitive closure; model checking},
language = {eng},
number = {2},
pages = {197-215},
publisher = {EDP-Sciences},
title = {Efficiency of automata in semi-commutation verification techniques},
url = {http://eudml.org/doc/245200},
volume = {42},
year = {2008},
}

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
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 $\cup _j$$L_{0,j}$$L_{1,j}$$L_{2,j}$$\ldots $$ 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$\mathcal {C}$, 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/245200
ER -

References

top
  1. [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. MR1729044
  2. [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. [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. Zbl1278.68150MR2081265
  4. [4] J. Berstel, Transductions and Context-Free Languages. B.G. Teubner, Stuttgart (1979). Zbl0424.68040MR549481
  5. [5] B. Boigelot and P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, in Proc. of 8 t h CAV (August), USA 1102 (1996) 1–12. 
  6. [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. MR1729031
  7. [7] A. Bouajjani, A. Muscholl and T. Touili, Permutation rewriting and algorithmic verification, in LICS’01. IEEE Comput. Soc. (2001) 399–408. Zbl1107.68052
  8. [8] J.A. Brzozowski, Hierarchies of aperiodic languages, 10 (1976) 33–49. Zbl0332.68056MR428813
  9. [9] J.A. Brzozowski and I. Simon, Characterizations of locally testable languages. 4 (1973) 243–271. Zbl0255.94032MR319404
  10. [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. [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). MR1470025
  12. [12] V. Diekert and G. Rozenberg, Ed. Book of Traces. World Scientific, Singapore (1995). MR1478992
  13. [13] Z. Esik and I. Simon, Modeling literal morphisms by shuffle. Semigroup Forum 56 (1998) 225–227. Zbl0982.20056MR1490294
  14. [14] P. Godefroid and P. Wolper, A partial approach to model checking. Inform. Comput. 110 (1994) 305–326. Zbl0806.68079MR1276739
  15. [15] A. Cano Gomez and J.-E. Pin, On a conjecture of schnoebelen, in DLT’03. (2003). Zbl1037.68075
  16. [16] A. Cano Gomez and J.-E. Pin, Shuffle on positive varieties of languages. 312 (2004) 433–461. Zbl1143.68431MR2028943
  17. [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. Zbl1102.68065MR2073244
  18. [18] P.-C. Héam, Some complexity results for polynomial rational expressions. 299 (2003). Zbl1042.68063MR1973175
  19. [19] J. Hopcroft and J. Ullman, Introduction to automata theory, languages, and computation. Addison-Wesley (1980). Zbl0426.68001MR645539
  20. [20] X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system, release 3.06. Inria, 2002. 
  21. [21] D. Lugiez and Ph. Schnoebelen, The regular viewpoint on pa-processes, in 9th Int. Conf. Concurrency Theory (CONCUR’98). . 1466 (1998). Zbl0932.68052MR1678717
  22. [22] J.-F. Perrot, Variété de langages et opérations. 7 (1978) 197–210. Zbl0398.68035MR509017
  23. [23] J.-E. Pin, Varieties of formal languages. Foundations of Computer Science (1984). Zbl0632.68069MR752695
  24. [24] J.-E. Pin and P. Weil, Polynomial closure and unambiguous product. Theor. Comput. Syst. 30 (1997) 1–39. Zbl0872.68119MR1450862
  25. [25] Ph. Schnoeboelen, Decomposable regular languages and the shuffle operator. EATCS Bull. 67 (1999) 283–289. 
  26. [26] H. Straubing, Finite semigroups varieties of the form V * D. 36 (1985) 53–94. Zbl0561.20042MR782639
  27. [27] P. Tesson and D. Thérien, Diamonds are forever: the variety da, in International Conference on Semigroups, Algorithms, Automata and Languages (2002). Zbl1031.20049MR2023803
  28. [28] W. Thomas, Classifying regular events in symbolic logic. 25 (1982) 360–375. Zbl0503.68055MR684265
  29. [29] D. Thérien, Classification of finite monoids: the language approach. 14 (1981) 195–208. Zbl0471.20055MR614416
  30. [30] T. Touili. Regular model checking using widening techniques, in 1st Vepas Workshop, volume 50 of Electronic Notes in TCS (2001). Zbl1262.68130

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.