  We present a theory of automata with boundary for designing, modelling and
analysing distributed systems. Notions of behaviour, design and simulation
appropriate to the theory are defined. The problem of model checking for
deadlock detection is discussed, and an algorithm for state space reduction in
exhaustive search, based on the theory presented here, is described. Three
examples of the application of the theory are given, one in the course of the
development of the ideas and two as illustrative examples of the use of the
theory.
