A Unified Approach to Language Containment and Fair CTL Model Checking

Two important practical approaches to formal verification of finite-state systems are language containment using L-automata (LC) ([Kur87, [Kur901]) and Computation Tree Logic model checking (MC) ([Cla86]). Using either method, abstraction is used to model hardware systems. In most cases, it becomes necessary to remove some of the traces of the system, introduced by abstraction. As constraints on the abstract models, one uses excepting conditions in LC, and fairness constraints in MC.