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

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

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 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
  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.  
  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.  
  4. J. Berstel, Transductions and Context-Free Languages. B.G. Teubner, Stuttgart (1979).  
  5. 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.  
  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.  
  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.  
  9. J.A. Brzozowski and I. Simon, Characterizations of locally testable languages. 4 (1973) 243–271.  
  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).  
  12. V. Diekert and G. Rozenberg, Ed. Book of Traces. World Scientific, Singapore (1995).  
  13. Z. Esik and I. Simon, Modeling literal morphisms by shuffle. Semigroup Forum56 (1998) 225–227.  
  14. P. Godefroid and P. Wolper, A partial approach to model checking. Inform. Comput.110 (1994) 305–326.  
  15. A. Cano Gomez and J.-E. Pin, On a conjecture of schnoebelen, in DLT'03. (2003).  
  16. A. Cano Gomez and J.-E. Pin, Shuffle on positive varieties of languages. 312 (2004) 433–461.  
  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.  
  18. P.-C. Héam, Some complexity results for polynomial rational expressions. 299 (2003).  
  19. J. Hopcroft and J. Ullman, Introduction to automata theory, languages, and computation. Addison-Wesley (1980).  
  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).  
  22. J.-F. Perrot, Variété de langages et opérations. 7 (1978) 197–210.  
  23. J.-E. Pin, Varieties of formal languages. Foundations of Computer Science (1984).  
  24. J.-E. Pin and P. Weil, Polynomial closure and unambiguous product. Theor. Comput. Syst.30 (1997) 1–39.  
  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.  
  27. P. Tesson and D. Thérien, Diamonds are forever: the variety da, in International Conference on Semigroups, Algorithms, Automata and Languages (2002).  
  28. W. Thomas, Classifying regular events in symbolic logic. 25 (1982) 360–375.  
  29. D. Thérien, Classification of finite monoids: the language approach. 14 (1981) 195–208.  
  30. T. Touili. Regular model checking using widening techniques, in 1st Vepas Workshop, volume 50 of Electronic Notes in TCS (2001).  

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.