Hi Philip,

Philip Schwartz pschwartz090@gmail.com writes:

If I have a deterministic automata and an LTL or python function which gets a word and return T/F.

Is it possible to set model checking for the dfa? to get a counterexample which distinguishes the dfa and the LTL/ python target function?

I'm not sure what this means. The LTL formula can be converted into an automaton. If you want to know if that automaton intersects another one, you can call aut1.intersects(aut2), that usually what model checkers do. The variant aut1.intersecting_word(aut2) will return a word accepted by both automata. To obtain a word that is accepted by one automaton and rejected by the other one, you may use aut1.exclusive_word(aut2).