Selected publications at LSV

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.

   author = {Bollig, Benedikt and Grindei, Manuela-Lidia and Habermehl, Peter},
   journal = {Formal Methods in System Design},
   note = {To appear},
   publisher = {Springer},
   title = {Realizability of Concurrent Recursive Programs},
   year = {2017},

About LSV

Select by Year