Hi, I have used the version 2.0 of your online tool for LTL to Buchi automata translation. At the time the tool did not return a deterministic Buchi automaton, but the new version does the transformation with ease. I was wondering if something fundamental has changed in your code that made this possible. Do you have the Changelog from 2.0 to 2.8? Here is the formula i used :
G(!e) & G((c&!d&Fd)->(p Ud)) & G(a&!c->(!c W(b&!c))) & GF(a)&GF(b)&GF(c)&GF(d)
RegardsHadi Zibaeenejad,PhDUniversity of Waterloo