Synthesis from Satisficing and Temporal Goals

TL;DR

This paper introduces a sound algorithm for reactive synthesis from high-level specifications combining LTL constraints and discounted-sum rewards with fractional discount factors, advancing planning and reinforcement learning applications.

Contribution

It extends previous satisficing approaches to handle fractional discount factors, providing the first sound algorithm for this setting.

Findings

Algorithm demonstrated on robotic planning domains

First sound method for fractional discount factors in synthesis

Improves applicability of LTL and DS rewards synthesis

Abstract

Reactive synthesis from high-level specifications that combine hard constraints expressed in Linear Temporal Logic LTL with soft constraints expressed by discounted-sum (DS) rewards has applications in planning and reinforcement learning. An existing approach combines techniques from LTL synthesis with optimization for the DS rewards but has failed to yield a sound algorithm. An alternative approach combining LTL synthesis with satisficing DS rewards (rewards that achieve a threshold) is sound and complete for integer discount factors, but, in practice, a fractional discount factor is desired. This work extends the existing satisficing approach, presenting the first sound algorithm for synthesis from LTL and DS rewards with fractional discount factors. The utility of our algorithm is demonstrated on robotic planning domains.