Distributed synthesis for parameterized temporal logics

DOI10.1016/J.IC.2018.09.009MaRDI QIDQ1784965zbMATH OpenOpenAlexWikidataFDO

Authors Swen Jacobs, Leander Tentrup, Martín G. Zimmermann

Publication date 27 September 2018

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1705.08112

zbMATH Keywords

incomplete informationparametric linear temporal logicdistributed synthesisdistributed realizabilityparametric linear dynamic logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Distributed PROMPT-LTL synthesis
• Parameterized synthesis
• Parameterized Synthesis
• Synthesis of Asynchronous Systems
• Distributed Synthesis for Alternating-Time Logics

Cites work

• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 1754607 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Assume-Guarantee Synthesis
• Assume-guarantee synthesis for concurrent reactive programs with partial information
• Detecting unrealizability of distributed fault-tolerant systems
• Distributed PROMPT-LTL synthesis
• Distributed synthesis for regular and contextfree specifications
• Distributed synthesis for well-connected architectures
• Distributed synthesis is simply undecidable
• Encodings of bounded synthesis
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Fair synthesis for asynchronous distributed systems
• From liveness to promptness
• Optimal bounds in parametric LTL games
• Parameterized Synthesis
• Parameterized linear temporal logics meet costs: still not costlier than LTL
• Parametric linear dynamic logic
• Parametric temporal logic for “model measuring”
• Reasoning about infinite computations
• Regular Linear Temporal Logic
• Synthesis of Asynchronous Systems
• Temporal logic can be more expressive
• Towards efficient parameterized synthesis

Cited in

(8)

• scientific article; zbMATH DE number 7085031 (Why is no real title available?)
• Distributed PROMPT-LTL synthesis
• scientific article; zbMATH DE number 1302050 (Why is no real title available?)
• Parameterized synthesis
• Distributed Synthesis for Alternating-Time Logics
• Towards efficient parameterized synthesis
• scientific article; zbMATH DE number 4112564 (Why is no real title available?)
• Parameter Synthesis for Timed Kripke Structures

This page was built for publication: Distributed synthesis for parameterized temporal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1784965)