Concurrent Program Schemes and their Interpretations

Abstract

Schemes of concurrent programs are considered. The result of a scheme is defined as a set of traces, where each trace is a partially ordered set of symbol occurrences. It is shown that to each scheme corresponds a set of equations determining the result of the scheme; it is shown how these equations can be solved and that the solutions of these equations are regular trace languages. Next, a notion of action systems is introduced; an action consists of its resources and its transformation. Some properties of action systems are shown. Interpretations of schemes are defined as mappings which assign actions to scheme symbols. Interpreted schemes can be regarded as concurrent programs. It is shown how the results of schemes can be lifted (via interpretations) to the results of programs. Some examples of applications of the described methods to prove concurrent programs correct are given.