A Finite Equational Base for CCS with Left Merge and Communication Merge
Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, and Bas Luttik

TL;DR
This paper develops a finite set of equations that completely characterizes the algebraic properties of a fragment of CCS, incorporating left merge and communication merge, especially when the set of actions is finite.
Contribution
It introduces a finite, ground-complete, and ω-complete equational base for CCS with specific operators, extending algebraic understanding of process calculi.
Findings
Finite equational base for CCS fragment established
Equational base is ground-complete and ω-complete
Base is finite when the set of actions is finite
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 recursion, restriction and relabelling. Our equational base is finite if the set of actions is finite.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · semigroups and automata theory
