We consider the process theory $PA$ that includes an operation for parallel composition, based on the interleaving paradigm. We prove that the standard set of axioms of $PA$ is not $omega$-complete by providing a set of axioms that are valid in $PA$, but not derivable from the standard ones. We prove that extending $PA$ with this set yields an $omega$-complete specification, which is finite in a setting with finitely many actions.

, ,
, ,
Software Engineering [SEN]
Software Analysis and Transformation

Fokkink, W., & Luttik, B. (2000). An $ omega $-complete equational specification of interleaving. Software Engineering [SEN]. CWI.