Abstract
A generalization of Kleene Algebras (structures with +·*, 0 and 1 operators) is considered to take into account possible nondeterminism expressed by the + operator. It is shown that essentially the same complete axiomatization of Salomaa is obtained except for the elimination of the distribution P·(Q + R) = P·Q + P·R and the idempotence law P + P = P. The main result is that an algebra obtained from a suitable category of labelled trees plays the same role as the algebra of regular events. The algebraic semantics and the axiomatization are then extended by adding Ω and ∥ operator, and the whole set of laws is used as a touchstone for starting a discussion over the laws for deadlock, termination and divergence proposed for models of concurrent systems.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Aceto,L., Hennessy,H.: Termination, Deadlock and Divergence, Journal of ACM, 39, 1, 1992, 147–187.
Baeten,J., van Glabbeek,R.: Abstraction and Empty Process in Process Algebras, Fundamenta Informaticae, XII, 1989, 221–242.
Bergstra,J.A., Klop,J.W.: Process Theory based Bisimulation Semantics, in LNCS 354; 1989, pp. 50–122.
Bergstra, J.A., Klop, J.W., Olderog, E.-R.: Failures without Chaos: A new Process Semantics for Fair Abstraction, in Formal Description of Programming Concepts III (M. Wirsing, Ed.), North Holland, Amsterdam 1987, pp. 77–103.
Benson,D.B., Tiuryn.J.: Fixed Points in Free Process Algebras-Part I, in Theoretical Computer Science, 63 (1989), 274–294.
Baeten, J., Weijland, P.: Process Algebras, Cambridge University Press, 1990.
De Nicola, R., Labella, A.: A Functorial Assessment of Bisimulation, Internal Report, Università di Roma La Sapienza, SI-92-06, 1992.
M. Hennessy, R. Milner: Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM, 32 (1985), 137–161.
C.A.R. Hoare: Communicating Sequential Processes, Prentice Hall, 1989.
Kleene, S.C.: 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, in Journal of Pure and Applied Algebra, 83 (1992), 295–321.
Kozen, D.: A Completeness Theorem for Kleene Algebras and the Algebras of Regular Events, in Proc. LICS '91, IEEE Press (1991), 214–225.
Milner, R.: Communication and Concurrency, Prentice Hall, 1989.
Park, D.: Concurrency and Automata on Infinite sequences, in Proc. GI, LNCS 104, Springer-Verlag, 1981; pp. 167–183.
Rutten, J. Explicit Canonical Representative for Weak Bisimulation Equivalences and Congruence, Draft, October 1990.
Salomaa, A.: Two Complete Axiom Systems for the Algebra of Regular Events, in Journal of A CM 13 (1966), 158–169.
Smith, M.B., Plotkin, D.. The category-Theoretic Solution of Recursive Domain Equation, SIAM Journal on Computing 11, 4, 1982, 762–783.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Nicola, R., Labella, A. (1994). A completeness theorem for nondeterministic Kleene algebras. In: Prívara, I., Rovan, B., Ruzička, P. (eds) Mathematical Foundations of Computer Science 1994. MFCS 1994. Lecture Notes in Computer Science, vol 841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58338-6_100
Download citation
DOI: https://doi.org/10.1007/3-540-58338-6_100
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58338-7
Online ISBN: 978-3-540-48663-3
eBook Packages: Springer Book Archive