Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-24T17:02:32.707Z Has data issue: false hasContentIssue false
  • English
  • Français

A Finite Axiomatization of Nondeterministic Regular Expressions

Published online by Cambridge University Press:  15 August 2002

Flavio Corradini ,
Rocco De Nicola  and
Anna Labella
Flavio Corradini
Affiliation:
Università dell'Aquila, Dipartimento di Matematica Pura ed Applicata, Via Vetoio, Loc. Coppito, I-67100 L'Aquila, Italy; [email protected].
Rocco De Nicola
Affiliation:
Università di Firenze, Dipartimento di Sistemi e Informatica, Via C. Lombroso 6/17, 50134 Firenze, Italy; [email protected].
Anna Labella
Affiliation:
Università di Roma “La Sapienza”, Dipartimento di Scienze dell'Informazione, Via Salaria 113, 00198 Roma, Italy; [email protected].
Get access

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

Keywords

Semanticsregular expressionsaxiomatizationsbisimulation.
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 33 , Issue 4-5 , July 1999 , pp. 447 - 465
Copyright
© EDP Sciences, 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aceto, L. and Fokkink, W., Equational Axiomatization, An for multi-exit iteration. Inform. and Comput. 134 (1997) 121-158. CrossRef
Aceto, L., Fokkink, W., van Glabbeek, R. and Ingólfsdóttir, A., Axiomatizing prefix iteration with silent steps. Inform. and Comput. 127 (1996) 26-40. CrossRef
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).
Baeten, J.C.M. and Bergstra, J.A., Process Algebra with a Zero Object, in Proc. of Concur'90. Springer, Lecture Notes in Comput. Sci. 458 (1990) 83-98. CrossRef
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.
S.L. Bloom and Z. Ésik, Iteration Algebras of Finite State Process Behaviours. Manuscript.
Bloom, S.L., Ésik, Z. and Taubner, D., Iteration theories of synchronization trees. Inform. and Comput. 102 (1993) 1-55. CrossRef
Boffa, M., Une remarque sur les systèmes complets d'identités rationelles. Theoret. Informatics Appl. 24 (1990) 419-423. CrossRef
J.H. Conway, Regular Algebra and Finite Machines. Chapman and Hall, London (1971).
F. Corradini, R. De Nicola and A. Labella, Fully Abstract Models for Nondeterministic Regular Expressions, in Proc. of Concur'95. Springer Verlag, Lecture Notes in Comput. Sci. 962 (1995) 130-144.
F. Corradini, R. De Nicola and A. Labella, Models of Nondeterministic Regular Expressions. J. Comput. System Sci., to appear.
R. De Nicola and A. Labella, Tree Morphisms and Bisimulations, in Proc. of MFCS'98 Workshop on Concurrency. Elsevier, Amsterdam, Electron. Notes Theoret. Comput. Sci. 18 (1998).
R. De Nicola and A. Labella, A Completeness Theorem for Nondeterministic Kleene Algebras, in Proc. of MFCS'94. Springer, Lecture Notes in Comput. Sci. 841 (1994) 536-545.
Fokkink, W., A complete equational axiomatization for prefix iteration. Inform. Process. Lett. 52 (1994) 333-337. CrossRef
W. Fokkink, On the completeness of the Equations for the Kleene Star in Bisimulation, in Proc. of AMAST'96. Springer, Lecture Notes in Comput. Sci. 1101 (1996) 180-194.
W. Fokkink, Axiomatizations for the perpetual loop in Process Algebras, in Proc. of ICALP'97. Springer, Lecture Notes in Comput. Sci. 1256 (1997) 571-581.
Fokkink, W. and Zantema, H., Basic process algebra with iteration: Completeness of its equational axioms. Comput. J. 37 (1994) 259-267. CrossRef
C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall (1989).
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.
Kasangian, S. and Labella, A., Enriched Categorical Semantics for Distributed Calculi. J. Pure Appl. Algebra 83 (1992) 295-321. CrossRef
Kozen, D., Completeness Theorem, A for Kleene Algebras and the Algebra of Regular Events. Inform. and Comput. 110 (1994) 366-390. CrossRef
Krob, D., Complete systems of B-rational identities. Theoret. Comput. Sci. 89 (1991) 207-343. CrossRef
W. Kuich and A. Salomaa, Semirings, Automata, Languages. Springer, Berlin, Monogr. Theoret. Comput. Sci. EATCS Ser. 5 (1986).
R. Milner, A Calculus of Communicating Systems. Springer-Verlag, Berlin, Lecture Notes in Comput. Sci. 94 (1980).
Milner, R., A complete inference system for a class of regular behaviors. J. Comput. System Sci. 28 (1984) 439-466. CrossRef
R. Milner, Communication and Concurrency. Prentice Hall (1989).
R.N. Moll, M.A. Arbib and A.J. Kfoury, An Introduction to Formal Language Theory. Springer-Verlag, Berlin (1987).
D. Park, Concurrency and Automata on Infinite sequences, in Proc. GI. Springer, Lecture Notes in Comput. Sci. 104 (1981) 167-183.
B.C. Pierce, Basic Category Theory for Computer Scientists. The MIT Press (1991).
Redko, V.N., On defining relations for the algebra of regular events (Russian). Ukrain. Mat. Z. 16 (1964) 120-126.
J. Sakarovitch, Kleene's theorem revisited, in Proc. of Trends, techniques, and problems in theoretical computer science. Springer, Lecture Notes in Comput. Sci. 281 (1986) 39-50.
Salomaa, A., Two Complete Axiom Systems for the Algebra of Regular Events. J. ACM 13 (1966) 158-169. CrossRef
P. Sewell, Bisimulation is not finitely (first order) equationally axiomatisable, in Proc. of LICS'94 (1994).
Smith, M.B. and Plotkin, G.D., The category-Theoretic Solution of Recursive Domain Equation. SIAM J. Comput. 11 (1982) 762-783.
Troeger, D.R., Step bisimulation is pomset equivalence on a parallel language without explicit internal choice. Math. Structures Comput. Sci. 3 (1993) 25-62. CrossRef