Engineering an LTLf Synthesis Tool
Formal Languages and Automata Theory
2025-07-04 v1
Abstract
The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a given LTLf specification. We describe the implementation of an LTLf synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from LTLf to a DFA represented as an array of Binary Decision Diagrams (MTBDDs) sharing their nodes. This MTBDD-based representation can be interpreted directly as a reachability game that is solved on-the-fly during its construction.
Keywords
Cite
@article{arxiv.2507.02491,
title = {Engineering an LTLf Synthesis Tool},
author = {Alexandre Duret-Lutz and Shufang Zhu and Nir Piterman and Giuseppe de Giacomo and Moshe Y Vardi},
journal= {arXiv preprint arXiv:2507.02491},
year = {2025}
}