Fatma Faruq <ffaruq@gmail.com> writes:

Hi, I was wondering if someone could point me to resources in spot that show how to evaluate an LTL word or trace on an automaton. Or anyway to check whether a trace or word satisfies a particular LTL formula.

Hi Fatma, If you convert your word into another automaton, testing acceptance can be reduced to an intersection between your two automata. import spot aut = spot.translate('a U b') wrd = spot.parse_word('a&!b;a&!b;cycle{a&b;!a&!b}').as_automaton() print("aut {} wrd".format("accepts" if aut.intersects(wrd) else "rejects")) Alexandre