Transforming sequential systems into concurrent systems

A problem of concurrent system specification is studied. A functionally equivalent system is first specified, then a set of independent actions or abstract resources is devised, and, finally, this sequential system is transformed into an equivalent concurrent system. The method is based on the theory of path expressions. The notion of functional equivalence is formally defined and studied. Necessary and sufficient conditions, stating when the method can be used, are formulated and proved. Some examples (vending machine, cigarette smokers, readers and writers, dining philosophers) are discussed.