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

Leander Tentrup
Alexander Weinert
Martin Zimmermann

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.

In Domenico Cantone and Giorgio Delzanno: Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016), Catania, Italy, 14-16 September 2016, Electronic Proceedings in Theoretical Computer Science 226, pp. 302–315.
Published: 13th September 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.226.21 Ancillary files bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org