
22 Dec
2020
22 Dec
'20
2:20 p.m.
Hello, 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? Regards, Phillip