Distributed PROMPT-LTL Synthesis

TL;DR

This paper investigates the synthesis of distributed systems from PROMPT-LTL specifications, showing that for synchronous systems the complexity remains unchanged, and providing a semi-decision procedure for asynchronous systems.

Contribution

It demonstrates that distributed PROMPT-LTL synthesis for synchronous systems is not harder than LTL synthesis and introduces a semi-decision method for asynchronous systems.

Findings

Distributed PROMPT-LTL synthesis complexity matches LTL for synchronous systems.

A semi-decision procedure for asynchronous PROMPT-LTL synthesis is proposed.

The approach handles scheduling assumptions in asynchronous settings.

Abstract

We consider the synthesis of distributed implementations for specifications in Prompt Linear Temporal Logic (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 systems, we show that, despite being more powerful, the distributed realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to consider an assume-guarantee synthesis problem, as we have to express scheduling assumptions. 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.