Distributed synthesis for parameterized temporal logics

DOI10.1016/J.IC.2018.09.009zbMATH Open1400.68124arXiv1705.08112OpenAlexW2963025247WikidataQ129189195 ScholiaQ129189195MaRDI QIDQ1784965FDOQ1784965

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

Publication date: 27 September 2018

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

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.

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

Recommendations

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

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)

Cites Work

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

Cited In (8)

• Title not available (Why is that?)
• Distributed Synthesis for Alternating-Time Logics
• Parameter Synthesis for Timed Kripke Structures
• Towards efficient parameterized synthesis
• Title not available (Why is that?)
• Distributed PROMPT-LTL synthesis
• Title not available (Why is that?)
• Parameterized synthesis

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)