# Distributed Synthesis for Parameterized Temporal Logics

## TL;DR

This paper investigates the synthesis of distributed systems from parameterized temporal logic specifications, showing that certain problems remain decidable or semi-decidable in various system models and extending results to stronger logics.

## Contribution

It demonstrates that distributed synthesis for PROMPT-LTL is not harder than LTL in synchronous systems and provides a semi-decision procedure for asynchronous systems, extending to PLTL and PLDL.

## Key findings

- Realizability for PROMPT-LTL in synchronous systems is as tractable as LTL.
- Semi-decision procedure for asynchronous PROMPT-LTL synthesis based on bounded synthesis.
- Results extend to stronger logics PLTL and PLDL.

## Abstract

We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which 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 distributed systems we show that, despite being more powerful, the realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to express scheduling assumptions and therefore consider an assume-guarantee synthesis problem. As asynchronous distributed synthesis is already undecidable for LTL, we give a semi-decision procedure for the PROMPT-LTL assume-guarantee synthesis problem based on bounded synthesis. Finally, we show that our results extend to the stronger logics PLTL and PLDL.