# Discounting in LTL

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jun 2014.

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

- [DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL](https://mlsanity.com/paper/2410.04631/) (2024)
- [Policy Synthesis and Reinforcement Learning for Discounted LTL](https://mlsanity.com/paper/2305.17115/) (2023)
- [Controller Synthesis for Omega-Regular and Steady-State Specifications](https://mlsanity.com/paper/2106.02951/) (2021)
- [Reinforcement Learning with Depreciating Assets](https://mlsanity.com/paper/2302.14176/) (2023)
- [Discounting in Strategy Logic](https://mlsanity.com/paper/2305.15256/) (2023)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)

## Abstract (arXiv)

In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given specification, reasoning about quality addresses the question of how well the system satisfies the specification. One direction in this effort is to refine the "eventually" operators of temporal logic to em discounting operators: the satisfaction value of a specification is a value in [0,1], where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is. In this paper we introduce an augmentation by discounting of Linear Temporal Logic (LTL), and study it, as well as its combination with propositional quality operators. We show that one can augment LTL with an arbitrary set of discounting functions, while preserving the decidability of the model-checking problem. Further augmenting the logic with unary propositional quality operators preserves decidability, whereas adding an average-operator makes some problems undecidable. We also discuss the complexity of the problem, as well as various extensions.