---
title: "Synthesizing Good-Enough Strategies for LTLf Specifications"
authors:
  - "Yong Li"
  - "Andrea Turrini"
  - "Moshe Y. Vardi"
  - "Lijun Zhang"
doi: "10.24963/ijcai.2021/570"
url: "https://ijcai.org/proceedings/2021/570"
pdf: "https://ijcai.org/proceedings/2021/0570.pdf"
venue: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence"
year: 2021
pages: "4144-4151"
track: "Main Track"
keywords:
  - "Planning and Scheduling: Applications of Planning"
  - "Planning and Scheduling: Temporal and Hybrid Planning"
  - "Planning and Scheduling: Planning and Scheduling"
---

# Synthesizing Good-Enough Strategies for LTLf Specifications

Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang

*Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence*, pages 4144-4151. DOI: [10.24963/ijcai.2021/570](https://doi.org/10.24963/ijcai.2021/570)

## Abstract

We consider the problem of synthesizing good-enough (GE)-strategies for linear temporal logic (LTL) over finite traces or LTLf for short.
The problem of synthesizing GE-strategies for an LTL formula φ over infinite traces reduces to the problem of synthesizing winning strategies for the formula (∃Oφ)⇒φ where O is the set of propositions controlled by the system.
We first prove that this reduction does not work for LTLf formulas.
Then we show how to synthesize GE-strategies for LTLf formulas via the Good-Enough (GE)-synthesis of LTL formulas.
Unfortunately, this requires to construct deterministic parity automata on infinite words, which is computationally expensive.
We then show how to synthesize GE-strategies for LTLf formulas by a reduction to solving games played on deterministic Büchi automata, based on an easier construction of deterministic automata on finite words.
We show empirically that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude.