CISPA
Browse
cispa_all_2743.pdf (388.83 kB)

Distributed synthesis for parameterized temporal logics

Download (388.83 kB)
journal contribution
posted on 2023-11-29, 18:07 authored by Swen JacobsSwen Jacobs, Leander Tentrup, Martin Zimmermann
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.

History

Preferred Citation

Swen Jacobs, Leander Tentrup and Martin Zimmermann. Distributed synthesis for parameterized temporal logics. In: Information and Computation. 2018.

Primary Research Area

  • Reliable Security Guarantees

Legacy Posted Date

2018-11-26

Journal

Information and Computation

Pages

311 - 328

Open Access Type

  • Unknown

Sub Type

  • Article

BibTeX

@article{cispa_all_2743, title = "Distributed synthesis for parameterized temporal logics", author = "Jacobs, Swen and Tentrup, Leander and Zimmermann, Martin", journal="{Information and Computation}", year="2018", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC