Realizability of concurrent recursive programs

We study the realizability problem for concurrent recursive programs: given a distributed system architecture and a sequential specification over words, find a distributed automata implementation that is equivalent to the specification. This problem is well-studied as far as finite-state processes are concerned, and it has a solution in terms of Zielonka’s Theorem. We lift Zielonka’s Theorem to the case where processes are recursive and modeled as visibly pushdown (or, equivalently, nested-word) automata. However, contrarily to the finite-state case, it is undecidable whether a specification is realizable or not. Therefore, we also consider suitable underapproximation techniques from the literature developed for multi-pushdown systems, and we show that they lead to a realizability framework with effective algorithms.