Distributed and Parametric Synthesis
Swen Jacobs, Leander Tentrup, Martín Zimmermann · arXiv (Cornell University) · 2015
We consider the synthesis of distributed implementations for specifications in Parametric Linear Temporal Logic (PLTL). PLTL extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous systems, we show that, despite being more powerful, the distributed realizability problem for PLTL is not harder than its LTL counterpart. The case of asynchronous systems requires assumptions on the scheduler beyond fairness to ensure that bounds can be met at all, i.e., even fair schedulers can delay processes arbitrary long and thereby prevent the system from satisfying its PLTL specification. Thus, we employ the concept of bounded fair scheduling, where every process is guaranteed to be scheduled in bounded intervals and give a semi-decision procedure for the resulting distributed assume-guarantee realizability problem.