An $ omega $-complete equational specification of interleaving
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.
|Concurrent Programming (acm D.1.3), Models of Computation (acm F.1.1), Modes of Computation (acm F.1.2)|
|Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Abstract data types; algebraic specification (msc 68Q65), Algebraic theory of languages and automata (msc 68Q70)|
|Software (theme 1)|
|Software Engineering [SEN]|
|Organisation||Software Analysis and Transformation|
Fokkink, W.J, & Luttik, S.P. (2000). An $ omega $-complete equational specification of interleaving. Software Engineering [SEN]. CWI.