The innovations in reactive synthesis from {\em Linear Temporal Logics over finite traces} (LTLf) will be amplified by the ability to verify the correctness of the strategies generated by LTLf synthesis tools. This motivates our work on {\em LTLf model checking}. LTLf model checking, however, is not straightforward. The strategies generated by LTLf synthesis may be represented using {\em terminating} transducers or {\em non-terminating} transducers where executions are of finite-but-unbounded length or infinite length, respectively. For synthesis, there is no evidence that one type of transducer is better than the other since they both demonstrate the same complexity and similar algorithms. In this work, we show that for model checking, the two types of transducers are fundamentally different. Our central result is that LTLf model checking of non-terminating transducers is \emph{exponentially harder} than that of terminating transducers. We show that the problems are EXPSPACE-complete and PSPACE-complete, respectively. Hence, considering the feasibility of verification, LTLf synthesis tools should synthesize terminating transducers. This is, to the best of our knowledge, the \emph{first} evidence to use one transducer over the other in LTLf synthesis.

翻译：基于有限迹的线性时序逻辑（LTLf）反应式综合中的创新将通过验证LTLf综合工具生成策略的正确性得到增强，这推动了我们对LTLf模型检测的研究。然而，LTLf模型检测并非直截了当。LTLf综合生成的策略可能使用“终止型”转换器或“非终止型”转换器表示，其中执行长度分别为有限但有界或无限长度。对于综合而言，尚无证据表明一种转换器优于另一种，因为两者具有相同的复杂度与相似的算法。本研究表明，对于模型检测，这两种转换器存在根本差异。核心结果是：非终止型转换器的LTLf模型检测比终止型转换器“指数级更困难”。我们证明这两个问题分别属于EXPSPACE完全与PSPACE完全。因此，基于验证的可行性，LTLf综合工具应合成终止型转换器。据我们所知，这是LTLf综合中为选择一种转换器而非另一种提供的“首个”证据。