A finite equational base for CCS with left merge and communication merge

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A finite equational base for CCS with left merge and communication merge

Full text

Pdf (224 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 1 (January 2009) table of contents

Article No. 6

Year of Publication: 2009

ISSN:1529-3785

Authors

Luca Aceto	Reykjavík University, Reykjavik, Iceland
Wan Fokkink	Vrije Universiteit Amsterdam and CWI, Amsterdam, The Netherlands
Anna Ingolfsdottir	Reykjavík University, Reykjavik, Iceland
Bas Luttik	Technische Universiteit Eindhoven and CWI, Eindhoven, The Netherlands

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 65, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1459010.1459016 What is a DOI?

ABSTRACT

Using the left merge and the 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 recursion, restriction and relabeling modulo (strong) bisimilarity. Our equational base is finite if the set of actions is finite.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Luca Aceto , Wan Fokkink , Anna Ingólfsdóttir , Bas Luttik, CCS with Hennessy's merge has no finite-equational axiomatization, Theoretical Computer Science, v.330 n.3, p.377-405, 9 February 2005 [doi>10.1016/j.tcs.2004.10.003]
	2	Aceto, L., Fokkink, W. J., Ingolfsdottir, A., and Luttik, B. 2005b. Finite equational bases in process algebra: Results and open questions. In Processes, Terms and Cycles: Steps on the Road to Infinity, A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R. C. de Vrijer, Eds. Lecture Notes in Computer Science, vol. 3838. Springer-Verlag, Berlin, Germany, 338--367.
	3	Jos C. M. Baeten , Mario Bravetti, A ground-complete axiomatization of finite state processes in process algebra, CONCUR 2005 - Concurrency Theory, Springer-Verlag, London, 2005 [doi>10.1007/11539452_21]
	4	Bergstra, J. A. and Klop, J. W. 1984. Process algebra for synchronous communication. Inform. Control 60, 1-3, 109--137.
	5	J. A. Bergstra , J. V. Tucker, Top-down design and the algebra of communicating processes, Science of Computer Programming, v.5 n.2, p.171-199, June 1985
	6	Christensen, S., Hirshfeld, Y., and Moller, F. 1994. Decidable subsets of CCS. Comput. J. 37, 4, 233--242.
	7	de Simone, R. 1985. Higher-level synchronising devices in Meije-SCCS. Theoret. Comput. Sci. 37, 245--267.
	8	Jan Friso Groote, A New Strategy for Proving omega-Completeness applied to Process Algebra, Proceedings of the Theories of Concurrency: Unification and Extension, p.314-331, August 27-30, 1990
	9	J Heering, Partial evaluation and &ohgr;-completeness of algebraic specifications, Theoretical Computer Science, v.43 n.2-3, p.149-167, July 1986
	10	Matthew Hennessy, Axiomatising finite concurrent processes, SIAM Journal on Computing, v.17 n.5, p.997-1017, October 1988 [doi>10.1137/0217063]
	11	Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
	12	Bas Luttik , Vincent van Oostrom, Decomposition orders: another generalisation of the fundamental theorem of arithmetic, Theoretical Computer Science, v.335 n.2-3, p.147-186, 23 May 2005 [doi>10.1016/j.tcs.2004.11.019]
	13	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	14	Milner, R. 1984. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci. 28, 3, 439--466.
	15	R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	16	Robin Milner, A complete axiomatisation for observational congruence of finite-state behaviours, Information and Computation, v.81 n.2, p.227-247, May 1989 [doi>10.1016/0890-5401(89)90070-9]
	17	Robin Milner , Faron Moller, Unique decomposition of processes, Theoretical Computer Science, v.107 n.2, p.357-363, Jan. 18, 1993 [doi>10.1016/0304-3975(93)90176-T]
	18	Moller, F. 1989. Axioms for concurrency. Ph.D. dissertatish. University of Edinburgh, Edinburgh, UK.
	19	Moller, F. 1990. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS'90). IEEE Computer Society Press, Los Alamitos, CA, 142--153.
	20	David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
	21	Sewell, P. 1994. Bisimulation is not finitely (first order) equationally axiomatisable. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS'94). IEEE Computer Society Press, Los Alamitos, CA, 62--70.
	22	van Tilburg, P. J. A. 2007. Finite equational bases for CCS with restriction. M.S. thesis, Technische Universiteit Eindhoven.