Process semantics: Global axioms, compositional rules, and applications

Abstract

We present a set of global axioms and compositional rules for describing the semantics of concurrent processes. In our semantic model, a process is defined by a set of partially-ordered traces on ports. The global axioms serve to rule out pathological processes. The compositional rules are used to derive semantics of composite processes from the semantics of their component processes. We prove that the global axioms are preserved by the compositional rules. A sound and complete proof system for our semantics is given. Finally, we apply the semantic model to give a formal definition of a concurrent language with dynamic process creation and dynamic port bindings.