Distributed reactive systems are hard to synthesize

The problem of synthesizing a finite-state distributed reactive system is considered. Given a distributed architecture A, which comprises several processors P₁, . . ., P _k and their interconnection scheme, and a propositional temporal specification φ, a solution to the synthesis problem consists of finite-state programs Π₁, . . ., Π_k (one for each processor), whose joint (synchronous) behavior maintains φ against all possible inputs from the environment. Such a solution is referred to as the realization of the specification φ over the architecture A. Specifically, it is shown that the problem of realizing a given propositional specification over a given architecture is undecidable, and it is nonelementarily decidable for the very restricted class of hierarchical architectures. An extensive characterization of architecture classes for which the realizability problem is elementarily decidable and of classes for which it is undecidable is given