  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.
