Metraipolis › archive › dc_7cdc982b35cf

A note on the reduction from LTLf to LTL — arXiv:2609.00379

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.00379
License (as archived): CC0-1.0
Archived: 2026-10-17T07:19:20.498Z
SHA-256 of the archived text: 4642316b029a2f26073b88b93fe191f5eb01365ab940d9e60d06ebbd098759f6
Stable URL of this page: https://metraipolis.com/documento/dc_7cdc982b35cf

How to cite

A note on the reduction from LTLf to LTL — arXiv:2609.00379 — arXiv (en), https://arxiv.org/abs/2609.00379 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_7cdc982b35cf (Metraipolis archive dc_7cdc982b35cf, sha256 4642316b029a2f26073b88b93fe191f5eb01365ab940d9e60d06ebbd098759f6)

BibTeX

@misc{dc7cdc982b35cf,
  title = {A note on the reduction from LTLf to LTL — arXiv:2609.00379},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.00379},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_7cdc982b35cf; sha256 4642316b029a2f26073b88b93fe191f5eb01365ab940d9e60d06ebbd098759f6},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.00379. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

LTLf, a finite word variant of LTL, can be reduced to LTL by introducing a new atomic proposition indicating the prefix of the infinite words that correspond to the finite words that the original LTLf formula was considering. Such a reduction was originally proposed by De Giacomo and Vardi (IJCAI'13). However, while any LTL formula reduced from LTLf describes an obligation property in the hierarchy of Manna and Pnueli (PODC'90), the aforementioned reduction does not provide an LTL formula that belongs to the syntactic obligation fragment of LTL. This note shows how the reduction was fixed in Spot in order to ensure that the resulting LTL formula is always a syntactic obligation. Doing so allows algorithms specialized to syntactic obligation to be used on LTLf formulas. For instance, in previous work (CAV'26) we described a specialized translation from syntactic obligations to minimal, weak, deterministic Büchi automata that would not be usable with the original reduction.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-09-02 in cs.LO).
Categorie arXiv: Formal Languages and Automata Theory (cs.FL) ; Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2609.00379 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-17T07:07:50.006Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-09-02?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).