Towards language emptiness model checking for MDG

Automata-based model checking uses ω-automata as the unifying models of both the system and its specification, and tests the languages of automata for the system are contained in the languages of automata for the specification. MDG is a hardware verification package that uses multiway decision graphs which accepts abstract variables and uninterpreted functions. This paper, first, surveys the ω-automata based model checking approaches and multiway decision graphs functionalities, then addresses the feasibility and approaches of developing automata-based model checking in MDGs