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) and Computation Tree Logic model checking (MC). 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. In this paper, we argue that MC and LC are to some extent complementary. We then show how to perform both LC and MC in a unified environment, where the constraints can be a combination of excepting conditions and fairness constraints. We present an MC algorithm for Fair CTL, an extension of CTL capable of handling fairness constraints, which uses algorithms for LC as a subroutine. Advances made in LC checking can then be used to obtain an efficient algorithm. The algorithms have been implemented, and we comment on some experimental results.