Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time
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 mi...
Main Authors: | Leander Tentrup, Alexander Weinert, Martin Zimmermann |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2016-09-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1511.09450v3 |
Similar Items
-
Distributed PROMPT-LTL Synthesis
by: Swen Jacobs, et al.
Published: (2016-09-01) -
Optimal Bounds in Parametric LTL Games
by: Martin Zimmermann
Published: (2011-06-01) -
Model checking LTL properties over C programs with bounded traces
by: Morse, Jeremy, et al.
Published: (2013) -
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
by: Martin Zimmermann
Published: (2015-09-01) -
LTL-Specification of Counter Machines
by: Egor V. Kuzmin
Published: (2021-03-01)