Transformations of sequential specifications into concurrent specifications by synchronization guards

A transformation C of sequential specifications into concurrent specifications is defined. The sequential specification is in the form of a regular expression extended with a declaration of the actions that are independent and have the potential for concurrent execution. The concurrent specification is in the form of a product of regular expressions. It is proved that a concurrent specification resulting from the application of the transformation C to a sequential specification modified by inserting special actions, called synchronization guards, is behaviorally equivalent to the original specification. The programming language representation of a sequential specification is exemplified in a Pascal-like language, Banach.