First-order checking of ω - automata using MDGs

Multiway decision graph (MDG) based model checking outperforms other symbolic model checking methods since it uses variables of abstract sort and uninterpeted function symbols. However, it can only accept a few first-order formula patterns; this greatly limits its application. To overcome this limitation, this paper proposes an omega-automata based verification technique using MDGs. Experimental results are presented to show the efficiency of the proposed method.