Realizability of concurrent recursive programs |
| |
Authors: | Benedikt Bollig Manuela-Lidia Grindei Peter Habermehl |
| |
Affiliation: | 1.CNRS, LSV, ENS Paris-Saclay,Cachan Cedex,France;2.Université Paris Diderot (Paris 7), IRIF,Paris,France |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|