Is there any general result to show that which automaton is more succinct? I have a set of LTL properties and I would like to know (show) which automaton is more efficient in term of state number and edge number.
Non-deterministic Buchi vs Rabin: Automaton size for LTL->automaton
automata;linear temporal logic