Towards language emptiness model checking for MDG
Fang Wang, Sofiène Tahar · 2003
Automata-based model checking uses /spl omega/-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 /spl omega/-automata based model checking approaches and multiway decision graphs functionalities, then addresses the feasibility and approaches of developing automata-based model checking in MDGs.