Automaton-based model checking on finite traces


I want to check whether a formula in finite LTL is valid on a finite, linear trace.

For infite traces I would create a Kripke structure of the trace and a Büchi automaton for the negated formula, and check if the intersection is empty. Would this also work with a finite trace and formula in FLTL? I already tried adding another atomic proposition “alive” to the Kripke structure and automaton (like here https://spot.lrde.epita.fr/tut12.html). But how could I do it without this additional atomic proposition?