  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.
