Modern computing is heavily dependent on systems of loosely cooperating processes, whose knowledge of each other is limited to what can be inferred from local history of joint action.

This paper addresses the control problem for such processes. That is, it addresses the problem of identifying whether or not each process has a local controller that can guarantee that a specific local property will be satisfied by all joint behaviors of the collection of processes. The paper’s key result is that the control problem is undecidable for local reachability properties if there are three or more processes in the system, but decidable and EXPTIME-complete for two processes.

For the purpose of proof, loosely coupled automata (LCA) are defined as particular kinds of Zielonka automata (parallel compositions of finite automata that synchronize on shared actions). The control problem is formulated in terms of local reachability conditions for LCA by asking whether or not a set of processes of an LCA can be controlled so as to satisfy local reachability conditions. Since solving Post’s correspondence problem can be reduced to solving the control problem, the control problem is shown to be undecidable. This is the case even if the number of processes is restricted to three, if communication is only allowed between pairs of processes, and if only one process has a single state that is not fully controlled. Finally, it is shown that the control problem for LCA is decidable and EXPTIME-complete if the number of processes is limited to two.

This paper is likely to be of interest to anyone who would like a deeper understanding of the nature of loosely cooperating processes and of the inherent limitations on controllability of such processes. Although some prior knowledge of automata and the classical problems of computability is assumed, the proofs themselves are elegant and reasonably accessible.