0
$\begingroup$

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?

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

The nice thing about finite traces is that they end at some point. LTLf is now a logic in which you can only look into the future, and not in the past.

This means that you label every character in the word by which subformulas of your LTLf formula hold for a word starting from that character. You start with the last character and just apply the semantics of LTLf there. Then you do the same for the second-last character, where you can use the fact that for the last character, you already know which LTL subformulas hold.

And then you continue in this way until you hit the first letter. Once you are done with that, you know for all subformulas if they hold there. You just have to look at the whole formula as subformula and are done.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.