Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time



Tentrup, Leander, Weinert, Alexander and Zimmermann, Martin ORCID: 0000-0002-8038-2453
(2015) Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time. .

[img] Text
twz.pdf - Published version

Download (181kB) | Preview

Abstract

We consider the optimization variant of the realizability problem for Prompt Linear Temporal Logic, an extension of Linear Temporal Logic (LTL) by the prompt eventually operator whose scope is bounded by some parameter. In the realizability optimization problem, one is interested in computing the minimal such bound that allows to realize a given specification. It is known that this problem is solvable in triply-exponential time, but not whether it can be done in doubly-exponential time, i.e., whether it is just as hard as solving LTL realizability. We take a step towards resolving this problem by showing that the optimum can be approximated within a factor of two in doubly-exponential time. Also, we report on a proof-of-concept implementation of the algorithm based on bounded LTL synthesis, which computes the smallest implementation of a given specification. In our experiments, we observe a tradeoff between the size of the implementation and the bound it realizes. We investigate this tradeoff in the general case and prove upper bounds, which reduce the search space for the algorithm, and matching lower bounds.

Item Type: Conference or Workshop Item (Unspecified)
Additional Information: In Proceedings GandALF 2016, arXiv:1609.03648
Uncontrolled Keywords: cs.LO, cs.LO, cs.FL
Depositing User: Symplectic Admin
Date Deposited: 15 Jul 2019 12:53
Last Modified: 19 Jan 2023 00:37
DOI: 10.4204/eptcs.226.21
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3049692