Concurrent transition system semantics of process networks

Using concurrent transition systems [Sta86], we establish connections between three models of concurrent process networks, Kahn functions, input/output automata, and labeled processes. For each model, we define three kinds of algebraic operations On processes: the product operation, abstraction operations, and connection operations. We obtain ho-momorphic mappings, from input/output automata to labeled processes, and from a subalgebra (called "input/output processes") of labeled processes to Kahn functions. The proof that the latter mapping preserves connection operations amounts to a new proof of the "Kahn Principle." Our approach yields: (1) extremely simple definitions of the process operations; (2) a simple and natural proof of the Kahn Principle that does not require the use of "strategies" or "scheduling arguments"; (3) a semantic characterization of a large class of labeled processes for which the Kahn Principle is valid, (4) a convenient operational semantics for nondeterminate process networks.