Technical Report Number
It is shown that behavioral semantics of Hoare's Parallel Commands can be formally specified by an extension of the regular expression, augmented by the shuffle operation and the inverse shuffle operation. As a corollary of the above, it is also shown that the problems of behavioral equivalence and deadlock-detection are solvable for the Parallel Commands.
Kimura, Takayuki D., "Behavioral Abstraction of Communicating Sequential Processes" Report Number: WUCS-79-9 (1979). All Computer Science and Engineering Research.
Permanent URL: http://dx.doi.org/10.7936/K7VQ312P