English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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