Traversing automata with current state uncertainty under LTL${}_f$ constraints

Andrew Ryzhikov, Petra Wolf

In this paper, we consider a problem which we call LTL${}_f$ model checking on paths: given a DFA $\mathcal{A}$ and a formula $\varphi$ in LTL on finite traces, does there exist a word $w$…