Optimal Bounds in Parametric LTL Games

TL;DR

This paper introduces algorithms for solving parametric LTL games, determining optimal variable valuations for winning strategies, and analyzing win conditions across different valuation sets, all within doubly-exponential time.

Contribution

It presents the first algorithms for optimal bounds in parametric LTL games, extending LTL game solving to parameterized temporal operators without increasing complexity.

Findings

Algorithms run in doubly-exponential time

Optimal variable valuations can be computed

Deciding winning conditions for various valuation sets is possible

Abstract

We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as "PLTL" by Alur et al. and (in a different version called "PROMPT-LTL") by Kupferman et al.. We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games.