Near-Optimal Scheduling for LTL with Future Discounting

TL;DR

This paper introduces an algorithm for finding near-optimal schedulers in LTL with future discounting, addressing a complex search problem with applications in error recovery, even in undecidable extended settings.

Contribution

It provides the first algorithm for near-optimal scheduling in discounted LTL, including in extended propositional operator settings where model-checking is undecidable.

Findings

Algorithm successfully finds near-optimal paths in discounted LTL.

Works in extended settings with propositional quality operators.

Addresses a problem relevant to error recovery and system scheduling.

Abstract

We study the search problem for optimal schedulers for the linear temporal logic (LTL) with future discounting. The logic, introduced by Almagor, Boker and Kupferman, is a quantitative variant of LTL in which an event in the far future has only discounted contribution to a truth value (that is a real number in the unit interval [0, 1]). The precise problem we study---it naturally arises e.g. in search for a scheduler that recovers from an internal error state as soon as possible---is the following: given a Kripke frame, a formula and a number in [0, 1] called a margin, find a path of the Kripke frame that is optimal with respect to the formula up to the prescribed margin (a truly optimal path may not exist). We present an algorithm for the problem; it works even in the extended setting with propositional quality operators, a setting where (threshold) model-checking is known to be undecidable.