Port automata and the algebra of concurrent processes

摘要

We model a process—the unit of concurrent processing—as a port automaton, a certain type of nondeterministic sequential machine. We show how to compute the response of these automata, and study the properties of their port interconnections. We are motivated by the work of Milne and Milner, but eschew their use of domains, continuous functions, and power-domains. Instead we can use sets, maps and subsets by applying our theory of greatest fixpoints to the study of the response of nondeterministic machines.