In this paper, we consider a problem which we call LTL$_f$ model checking on paths: given a DFA $\mathcal{A}$ and a formula $\phi$ in LTL on finite traces, does there exist a word $w$ such that every path starting in a state of $\mathcal{A}$ and labeled by $w$ satisfies $\phi$? The original motivation for this problem comes from the constrained parts orienting problem, introduced in [Petra Wolf, "Synchronization Under Dynamic Constraints", FSTTCS 2020], where the input constraints restrict the order in which certain states are visited for the first or the last time while reading a word $w$ which is also required to synchronize $\mathcal{A}$. We identify very general conditions under which LTL$_f$ model checking on paths is solvable in polynomial space. For the particular constraints in the parts orienting problem, we consider PSPACE-complete cases and one NP-complete case. The former provide very strong lower bound for LTL$_f$ model checking on paths. The latter is related to (classical) LTL$_f$ model checking for formulas with the until modality only and with no nesting of operators. We also consider LTL$_f$ model checking of the power-set automaton of a given DFA, and get similar results for this setting. For all our problems, we consider the case where the required word must also be synchronizing, and prove that if the problem does not become trivial, then this additional constraint does not change the complexity.

翻译：本文研究一个称为路径上的LTL$_f$模型检测问题：给定一个DFA $\mathcal{A}$和一个关于有限迹的LTL公式$\phi$，是否存在一个单词$w$，使得从$\mathcal{A}$的任意状态出发、以$w$标记的每条路径都满足$\phi$？该问题的原始动机源于[Petra Wolf, "Synchronization Under Dynamic Constraints", FSTTCS 2020]中提出的约束零件定向问题，其中输入约束限制了在读取（同时需同步$\mathcal{A}$的）单词$w$时，某些状态首次或末次被访问的顺序。我们识别出路径上LTL$_f$模型检测可在多项式空间内求解的非常一般性条件。针对零件定向问题中的特定约束，我们考虑了PSPACE完全情形和一种NP完全情形：前者为路径上LTL$_f$模型检测提供了极强下界，后者与仅包含直到算子且算子无嵌套的（经典）LTL$_f$公式模型检测相关。本文还研究了给定DFA的幂集自动机上的LTL$_f$模型检测，并证明了类似结果。对所有问题，我们考虑了所需单词必须同时具有同步性的情形，并证明若问题非平凡，则此额外约束不改变问题复杂度。