标题： 工程化一个LTLf合成工具 显示英文标题

标题： Engineering an LTLf Synthesis Tool

摘要： LTLf反应综合问题是构建一个转换器，其输出基于输入的历史，使得对于每个输入的无限序列，输入和输出的联合演化有一个前缀满足给定的LTLf规范。 我们描述了一个LTLf综合器的实现，在我们的基准测试套件中，该实现优于现有的工具。 这是基于一种新的直接从LTLf到DFA的翻译，该DFA表示为共享节点的二进制决策图数组（MTBDD）。 这种基于MTBDD的表示可以直接解释为一个可达性博弈，在构造过程中实时求解。 显示英文摘要

摘要： 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.