Abstract
A classical result from Redko [20] says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema [13] showed, by means of a term rewriting analysis, that there does exist a complete finite equational axiomatization for the Kleene star up to strong bisimulation equivalence. This paper presents a simpler and shorter completeness proof. Furthermore, the result is extended to open terms, i.e., to ω-completeness. Finally, it is shown that the three equations for the Kleene star are all essential for completeness.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
L. Aceto. Personal communication, December 1995.
L. Aceto and W.J. Fokkink. A complete axiomatization for multi-exit iteration. In preparation.
L. Aceto, W.J. Fokkink, R.J. van Glabbeek, and A. Ingólfsdóttir. Axiomatizing prefix iteration with silent steps. Report RS-95-56, BRICS, University of Aalborg, 1995. To appear in Information and Computation.
J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the ACM, 40(3):653–682, 1993.
J.C.M. Baeten and C. Verhoef. A congruence theorem for structured operational semantics with predicates. In E. Best, ed., Proceedings CONCUR'93, Hildesheim, LNCS 715, pp. 477–492. Springer, 1993.
J.C.M. Baeten and C. Verhoef. Concrete process algebra. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, eds., Handbook of Logic in Computer Science, Volume IV, pp. 149–268. Oxford University Press, 1995.
J. A. Bergstra, I. Bethke, and A. Ponse. Process algebra with iteration and nesting. The Computer Journal, 37(4):243–258, 1994.
J.A. Bergstra and J.W. Klop. Verification of an alternating bit protocol by means of process algebra. In W. Bibel and K.P. Jantke, eds., Proceedings Mathematical Methods of Specification and Synthesis of Software Systems, Wendisch-Rietz, LNCS 215, pp. 9–23. Springer, 1985.
D. Caucal. Graphes canoniques et graphes algébriques. Theoretical Informatics and Applications, 24(4):339–352, 1990.
J.H. Conway. Regular algebra and finite machines. Chapman and Hall, 1971.
W.J. Fokkink. A complete equational axiomatization for prefix iteration. Information Processing Letters, 52(6):333–337, 1994.
W.J. Fokkink and R.J. van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Technical Note CS-95-17, Stanford University, 1995. To appear in Information and Computation.
W.J. Fokkink and H. Zantema. Basic process algebra with iteration: completeness of its equational axioms. The Computer Journal, 37(4):259–267, 1994.
R.J. van Glabbeek. A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In A.M. Borzyszkowski and S. Sokołowski, eds., Proceedings MFCS'93, Gdansk, LNCS 711, pp. 473–484. Springer, 1993.
S.C. Kleene. Representation of events in nerve nets and finite automata. In Automata Studies, pages 3–41. Princeton University Press, 1956.
R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28:439–466, 1984.
R. Milner. A complete axiomatisation for observational congruence of finite-state behaviors. Information and Computation, 81(2):227–247, 1989.
D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings 5th GI Conference, Karlsruhe, LNCS 104, pp. 167–183. Springer, 1981.
G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University, 1981.
V.N. Redko. On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal, 16:120–126, 1964. In Russian.
A. Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the ACM, 13(1):158–169, 1966.
P. Sewell. Bisimulation is not finitely (first order) equationally axiomatisable. In Proceedings LICS'94, Paris, pp. 62–70. IEEE Computer Society Press, 1994.
D.R. Troeger. Step bisimulation is pomset equivalence on a parallel language without explicit internal choice. Mathematical Structures in Computer Science, 3:25–62, 1993.
H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24(1,2):89–105, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fokkink, W. (1996). On the completeness of the equations for the Kleene star in bisimulation. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014315
Download citation
DOI: https://doi.org/10.1007/BFb0014315
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61463-0
Online ISBN: 978-3-540-68595-1
eBook Packages: Springer Book Archive