Duret-Lutz, Alexandre 
ORCID: 0000-0002-6623-2512, Zhu, Shufang ORCID: 0000-0002-5922-8750, Piterman, Nir ORCID: 0000-0002-8242-5357, De Giacomo, Giuseppe ORCID: 0000-0001-9680-7658 and Vardi, Moshe Y ORCID: 0000-0002-0661-5773
(2026)
Engineering an $$\mathsf {LTL_f}$$ Synthesis Tool.
Lecture Notes in Computer Science, 15981.
pp. 129-147.
ISSN 0302-9743, 1611-3349
|
Text
Engineering_an_LTLf (1).pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (862kB) | Preview |
Abstract
The problem of LTL<inf>f</inf> 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 LTL<inf>f</inf> specification. We describe the implementation of an LTL<inf>f</inf> synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from LTL<inf>f</inf> 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.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | 46 Information and Computing Sciences, 4602 Artificial Intelligence |
| Divisions: | Faculty of Science and Engineering |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 23 Sep 2025 10:25 |
| Last Modified: | 23 Sep 2025 10:25 |
| DOI: | 10.1007/978-3-032-02602-6_10 |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3194571 |
Altmetric
Altmetric