# LTLf Synthesis on Probabilistic Systems

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Sep 2020.

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

- [Policy Synthesis and Reinforcement Learning for Discounted LTL](https://mlsanity.com/paper/2305.17115/) (2023)
- [Model Checking Strategies from Synthesis Over Finite Traces](https://mlsanity.com/paper/2305.08319/) (2023)
- [Mimicking Behaviors in Separated Domains](https://mlsanity.com/paper/2205.09201/) (2022)
- [Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees](https://mlsanity.com/paper/2303.12558/) (2023)
- [Composition of Nondeterministic and Stochastic Services for LTLf Task Specifications](https://mlsanity.com/paper/2311.18114/) (2023)

## Abstract (arXiv)

Many systems are naturally modeled as Markov Decision Processes (MDPs), combining probabilities and strategic actions. Given a model of a system as an MDP and some logical specification of system behavior, the goal of synthesis is to find a policy that maximizes the probability of achieving this behavior. A popular choice for defining behaviors is Linear Temporal Logic (LTL). Policy synthesis on MDPs for properties specified in LTL has been well studied. LTL, however, is defined over infinite traces, while many properties of interest are inherently finite. Linear Temporal Logic over finite traces (LTLf) has been used to express such properties, but no tools exist to solve policy synthesis for MDP behaviors given finite-trace properties. We present two algorithms for solving this synthesis problem: the first via reduction of LTLf to LTL and the second using native tools for LTLf. We compare the scalability of these two approaches for synthesis and show that the native approach offers better scalability compared to existing automaton generation tools for LTL.