Abstract
Using the left merge and communication merge from ACP, we present an equational base (i.e., a ground-complete and ω-complete set of valid equations) for the fragment of CCS without restriction and relabelling. Our equational base is finite if the set of actions is finite.
The first and third author were partly supported by the project “The Equational Logic of Parallel Processes” (nr. 060013021) of The Icelandic Research Fund.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aceto, L., Fokkink, W.J., Ingolfsdottir, A., Luttik, B.: CCS with Hennessy’s merge has no finite equational axiomatization. Theor. Comput. Sci. 330(3), 377–405 (2005)
Aceto, L., Fokkink, W.J., Ingólfsdóttir, A., Luttik, B.: Finite Equational Bases in Process Algebra: Results and Open Questions. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 338–367. Springer, Heidelberg (2005)
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inform. and Control 60(1-3), 109–137 (1984)
Bergstra, J.A., Tucker, J.V.: Top-down design and the algebra of communicating processes. Sci. Comput. Programming 5(2), 171–199 (1985)
de Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theor. Comput. Sci. 37, 245–267 (1985)
Groote, J.F.: A new strategy for proving ω-completeness applied to process algebra. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 314–331. Springer, Heidelberg (1990)
Heering, J.: Partial evaluation and ω-completeness of algebraic specifications. Theoret. Comput. Sci. 43(2-3), 149–167 (1986)
Hennessy, M.: Axiomatising finite concurrent processes. SIAM J. Comput. 17(5), 997–1017 (1988)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161,(January 1985)
Luttik, B., van Oostrom, V.: Decomposition orders—another proof of the fundamental theorem of arithmetic. Theor. Comput. Sci. 335(2–3), 147–186 (2005)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Moller, F.: Axioms for Concurrency. PhD thesis, University of Edinburgh (1989)
Moller, F.: The nonexistence of finite axiomatisations for CCS congruences. In: Proceedings of LICS1990, pp. 142–153. IEEE Computer Society Press, Los Alamitos (1990)
Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Taylor, W.: Equational logic. Houston J. Math (Survey) (1979)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Fokkink, W., Ingolfsdottir, A., Luttik, B. (2006). A Finite Equational Base for CCS with Left Merge and Communication Merge. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds) Automata, Languages and Programming. ICALP 2006. Lecture Notes in Computer Science, vol 4052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11787006_42
Download citation
DOI: https://doi.org/10.1007/11787006_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35907-4
Online ISBN: 978-3-540-35908-1
eBook Packages: Computer ScienceComputer Science (R0)