Small Deterministic Automata for LTL\GU
Jan Kret ́ insky, Ruslán Ledesma Garza · 2013
We present a tool that generates automata for LTL(X,F,G,U )w hereU does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of mag- nitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.