关于LTLf到LTL归约的一个注记
A note on the reduction from LTLf to LTL
中文总结 AI 辅助
该注记修正了Spot中LTLf到LTL的归约，使结果LTL公式为句法义务，从而可将句法义务专用算法应用于LTLf公式，支持此前无法通过原始归约实现的专用翻译。
中文摘要 AI 辅助
LTLf是LTL的有限字变体，可通过引入新原子命题归约为LTL，该命题表示与原LTLf公式所考虑的有限字对应的无限字的前缀，此归约最初由De Giacomo和Vardi（IJCAI'13）提出。然而，尽管从LTLf归约得到的任何LTL公式都描述了Manna和Pnueli（PODC'90）层次中的义务属性，但上述归约并未提供属于LTL句法义务片段的LTL公式。本注记展示了Spot中如何修正该归约，以确保得到的LTL公式始终为句法义务，这使得专门针对句法义务的算法可应用于LTLf公式。例如，在之前的工作（CAV'26）中，我们描述了从句法义务到极小弱确定Büchi自动机的专门翻译，该翻译无法与原始归约配合使用。
英文摘要
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.
