# Synthesis from Satisficing and Temporal Goals

arXiv: https://arxiv.org/abs/2205.10464 · HTML: https://mlsanity.com/paper/2205.10464/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 28 references that are in the map.
- First posted on arXiv 20 May 2022.

## Builds on (most cited first, 5 of 5)

- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [Correct-by-synthesis reinforcement learning with temporal logic constraints](https://mlsanity.com/paper/1503.01793/) (2015)
- [Comparator automata in quantitative verification](https://mlsanity.com/paper/1812.06569/) (2018)
- [On Satisficing in Quantitative Games](https://mlsanity.com/paper/2101.02594/) (2021)

## Built on by (most cited first, 1 of 1)

- [Categorizer Automata for Discounted-Sum Payoffs](https://mlsanity.com/paper/2608.26763/) (2026)

## Abstract (arXiv)

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.