Behavioral Abstraction of Communicating Sequential Processes
Takayuki Dan Kimura · Open Scholarship Institutional Repository (Washington University in St. Louis) · 1979
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.