# 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?

• (When editing the question for whatever reason, replace infite.) – greybeard May 2 '20 at 19:02