A Finite Axiomatization of Nondeterministic Regular Expressions

Flavio Corradini; Rocco De Nicola; Anna Labella

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 4-5, page 447-465
  • ISSN: 0988-3754

Abstract

top
An alternative (tree-based) semantics for a class of regular expressions is proposed that assigns a central rôle to the + operator and thus to nondeterminism and nondeterministic choice. For the new semantics a consistent and complete axiomatization is obtained from the original axiomatization of regular expressions by Salomaa and by Kozen by dropping the idempotence law for + and the distribution law of • over +.

How to cite

top

Corradini, Flavio, De Nicola, Rocco, and Labella, Anna. "A Finite Axiomatization of Nondeterministic Regular Expressions." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 447-465. <http://eudml.org/doc/221958>.

@article{Corradini2010,
abstract = { An alternative (tree-based) semantics for a class of regular expressions is proposed that assigns a central rôle to the + operator and thus to nondeterminism and nondeterministic choice. For the new semantics a consistent and complete axiomatization is obtained from the original axiomatization of regular expressions by Salomaa and by Kozen by dropping the idempotence law for + and the distribution law of • over +. },
author = {Corradini, Flavio, De Nicola, Rocco, Labella, Anna},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Semantics; regular expressions; axiomatizations; bisimulation.; regular languages},
language = {eng},
month = {3},
number = {4-5},
pages = {447-465},
publisher = {EDP Sciences},
title = {A Finite Axiomatization of Nondeterministic Regular Expressions},
url = {http://eudml.org/doc/221958},
volume = {33},
year = {2010},
}

TY - JOUR
AU - Corradini, Flavio
AU - De Nicola, Rocco
AU - Labella, Anna
TI - A Finite Axiomatization of Nondeterministic Regular Expressions
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 4-5
SP - 447
EP - 465
AB - An alternative (tree-based) semantics for a class of regular expressions is proposed that assigns a central rôle to the + operator and thus to nondeterminism and nondeterministic choice. For the new semantics a consistent and complete axiomatization is obtained from the original axiomatization of regular expressions by Salomaa and by Kozen by dropping the idempotence law for + and the distribution law of • over +.
LA - eng
KW - Semantics; regular expressions; axiomatizations; bisimulation.; regular languages
UR - http://eudml.org/doc/221958
ER -

References

top
  1. L. Aceto and W. Fokkink, An Equational Axiomatization for multi-exit iteration. Inform. and Comput.134 (1997) 121-158.  Zbl0881.68069
  2. L. Aceto, W. Fokkink, R. van Glabbeek and A. Ingólfsdóttir, Axiomatizing prefix iteration with silent steps. Inform. and Comput.127 (1996) 26-40.  Zbl0855.68030
  3. L. Aceto, W. Fokkink and A. Ingólfsdóttir, A managerie of non-finitely based process semantics over BPA*: From ready simulation to completed traces. Research Report, BRICS, RS-96-23 (1996).  
  4. J.C.M. Baeten and J.A. Bergstra, Process Algebra with a Zero Object, in Proc. ofConcur'90. Springer, Lecture Notes in Comput. Sci.458 (1990) 83-98.  
  5. L. Bernatsky, S.L. Bloom, Z. Ésik and Gh. Stefanescu, Equational theories of relations and regular sets, in Proc. of Words, Languages and Combinatorics, Kyoto, 1992. Word Scientific, (1994) 40-48.  Zbl0874.08002
  6. S.L. Bloom and Z. Ésik, Iteration Algebras of Finite State Process Behaviours. Manuscript.  
  7. S.L. Bloom, Z. Ésik and D. Taubner, Iteration theories of synchronization trees. Inform. and Comput.102 (1993) 1-55.  Zbl0780.68088
  8. M. Boffa, Une remarque sur les systèmes complets d'identités rationelles. Theoret. Informatics Appl.24 (1990) 419-423.  Zbl0701.68059
  9. J.H. Conway, Regular Algebra and Finite Machines. Chapman and Hall, London (1971).  Zbl0231.94041
  10. F. Corradini, R. De Nicola and A. Labella, Fully Abstract Models for Nondeterministic Regular Expressions, in Proc. ofConcur'95. Springer Verlag, Lecture Notes in Comput. Sci. 962 (1995) 130-144.  
  11. F. Corradini, R. De Nicola and A. Labella, Models of Nondeterministic Regular Expressions. J. Comput. System Sci., to appear.  Zbl0958.68090
  12. R. De Nicola and A. Labella, Tree Morphisms and Bisimulations, in Proc. ofMFCS'98 Workshop on Concurrency. Elsevier, Amsterdam, Electron. Notes Theoret. Comput. Sci. 18 (1998).  
  13. R. De Nicola and A. Labella, A Completeness Theorem for Nondeterministic Kleene Algebras, in Proc. ofMFCS'94. Springer, Lecture Notes in Comput. Sci. 841 (1994) 536-545.  
  14. W. Fokkink, A complete equational axiomatization for prefix iteration. Inform. Process. Lett.52 (1994) 333-337.  Zbl0938.68697
  15. W. Fokkink, On the completeness of the Equations for the Kleene Star in Bisimulation, in Proc. ofAMAST'96. Springer, Lecture Notes in Comput. Sci. 1101 (1996) 180-194.  Zbl0886.03032
  16. W. Fokkink, Axiomatizations for the perpetual loop in Process Algebras, in Proc. ofICALP'97. Springer, Lecture Notes in Comput. Sci. 1256 (1997) 571-581.  
  17. W. Fokkink and H. Zantema, Basic process algebra with iteration: Completeness of its equational axioms. Comput. J.37 (1994) 259-267.  
  18. C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall (1989).  Zbl0383.68028
  19. S.C. Kleene, Representation of Events in Nerve Nets and Finite Automata, in Automata Studies, Shannon and McCarthy, Ed. Princeton Univ. Pr. (1956) 3-41.  
  20. S. Kasangian and A. Labella, Enriched Categorical Semantics for Distributed Calculi. J. Pure Appl. Algebra83 (1992) 295-321.  Zbl0777.18007
  21. D. Kozen, A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Inform. and Comput.110 (1994) 366-390.  Zbl0806.68082
  22. D. Krob, Complete systems of B-rational identities. Theoret. Comput. Sci.89 (1991) 207-343.  Zbl0737.68053
  23. W. Kuich and A. Salomaa, Semirings, Automata, Languages. Springer, Berlin, Monogr. Theoret. Comput. Sci. EATCS Ser.5 (1986).  
  24. R. Milner, A Calculus of Communicating Systems. Springer-Verlag, Berlin, Lecture Notes in Comput. Sci.94 (1980).  Zbl0452.68027
  25. R. Milner, A complete inference system for a class of regular behaviors. J. Comput. System Sci. 28 (1984) 439-466.  Zbl0562.68065
  26. R. Milner, Communication and Concurrency. Prentice Hall (1989).  
  27. R.N. Moll, M.A. Arbib and A.J. Kfoury, An Introduction to Formal Language Theory. Springer-Verlag, Berlin (1987).  Zbl0655.68002
  28. D. Park, Concurrency and Automata on Infinite sequences, in Proc. GI. Springer, Lecture Notes in Comput. Sci. 104 (1981) 167-183.  
  29. B.C. Pierce, Basic Category Theory for Computer Scientists. The MIT Press (1991).  Zbl0875.18001
  30. V.N. Redko, On defining relations for the algebra of regular events (Russian). Ukrain. Mat. Z.16 (1964) 120-126.  
  31. J. Sakarovitch, Kleene's theorem revisited, in Proc. ofTrends, techniques, and problems in theoretical computer science. Springer, Lecture Notes in Comput. Sci. 281 (1986) 39-50.  
  32. A. Salomaa, Two Complete Axiom Systems for the Algebra of Regular Events. J. ACM13 (1966) 158-169.  Zbl0149.24902
  33. P. Sewell, Bisimulation is not finitely (first order) equationally axiomatisable, in Proc. ofLICS'94 (1994).  
  34. M.B. Smith and G.D. Plotkin, The category-Theoretic Solution of Recursive Domain Equation. SIAM J. Comput.11 (1982) 762-783.  
  35. D.R. Troeger, Step bisimulation is pomset equivalence on a parallel language without explicit internal choice. Math. Structures Comput. Sci.3 (1993) 25-62.  Zbl0806.68044

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.