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.

翻译：从{\em 有限迹上的线性时序逻辑}（$\ltlf$）进行反应式合成的创新成果，将通过验证$\ltlf$合成工具生成策略正确性的能力得到放大。这推动了我们在{\em $\ltlf$模型检测}方面的研究。然而，$\ltlf$模型检测并非直接了当。$\ltlf$合成生成的策略既可使用{\em 终止型}换能器表示（执行序列为有限无界长度），也可使用{\em 非终止型}换能器表示（执行序列为无限长度）。在合成领域，由于两类换能器具有相同的复杂度和相似的算法，尚无证据表明某一类型优于另一类型。本文证明，在模型检测中这两类换能器存在根本性差异。我们的核心结论是：非终止型换能器的$\ltlf$模型检测比终止型换能器{\em 指数级更困难}。我们分别证明这两个问题属于\expspace-完备和$\pspace$-完备。因此，从验证可行性角度考虑，$\ltlf$合成工具应当采用终止型换能器。据我们所知，这是$\ltlf$合成中选择某一类型换能器的{\em 首个}理论依据。