Combining Local and Global Model Checking

✍ Scribed by Armin Biere; Edmund M. Clarke; Yunshan Zhu

• Publisher: Elsevier Science
• Year: 2001
• Tongue: English
• Weight: 658 KB
• Volume: 23
• Category: Article
• ISSN: 1571-0661
• DOI: 10.1016/s1571-0661(04)80667-4

✦ Synopsis

The veri cation process of reactive systems in local model checking 1,7] and in explicit state model checking 13,15] is on-the-y. Therefore only those states of a system have to be traversed that are necessary to prove a property. In addition, if the property does not hold, than often only a small subset of the state space has to be traversed to produce a counterexample. Global model checking 6,23] and, in particular, symbolic model checking 4,22] can utilize compact representations of the state space, e.g. BDDs 3], to handle much larger designs than what is possible with local and explicit model checking. We present a n e w m o d e l c hecking algorithm for LTL that combines both approaches. In essence, it is a generalization of the tableau construction of 1] that enables the use of BDDs but still is on-the-y.