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

TL;DR

This paper presents an approximation algorithm for the optimal bounds in Prompt-LTL realizability, reducing the complexity to doubly-exponential time and providing practical insights through implementation and experiments.

Contribution

It introduces a doubly-exponential time approximation method for Prompt-LTL realizability bounds, improving understanding of the problem's complexity and offering a practical implementation.

Findings

Approximation within a factor of two in doubly-exponential time.

Tradeoff between implementation size and bounds realized.

Upper and lower bounds for the search space.

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.