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.  Zbl1278.68150
  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.  Zbl1107.68052
  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.  Zbl0255.94032
  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.  Zbl0982.20056
  14. P. Godefroid and P. Wolper, A partial approach to model checking. Inform. Comput.110 (1994) 305–326.  Zbl0806.68079
  15. A. Cano Gomez and J.-E. Pin, On a conjecture of schnoebelen, in DLT'03. (2003).  Zbl1037.68075
  16. A. Cano Gomez and J.-E. Pin, Shuffle on positive varieties of languages. 312 (2004) 433–461.  Zbl1143.68431
  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.68065
  18. P.-C. Héam, Some complexity results for polynomial rational expressions. 299 (2003).  Zbl1042.68063
  19. J. Hopcroft and J. Ullman, Introduction to automata theory, languages, and computation. Addison-Wesley (1980).  Zbl0847.68065
  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).  Zbl0932.68052
  22. J.-F. Perrot, Variété de langages et opérations. 7 (1978) 197–210.  Zbl0398.68035
  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.  Zbl0872.68119
  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.  Zbl0561.20042
  27. P. Tesson and D. Thérien, Diamonds are forever: the variety da, in International Conference on Semigroups, Algorithms, Automata and Languages (2002).  Zbl1031.20049
  28. W. Thomas, Classifying regular events in symbolic logic. 25 (1982) 360–375.  Zbl0503.68055
  29. D. Thérien, Classification of finite monoids: the language approach. 14 (1981) 195–208.  Zbl0471.20055
  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.