Progress on the State Explosion Problem in Model Checking

摘要: Model checking is an automatic verification technique for finite state concurrent systems. In this approach to verification, temporal logic specifications are checked by exhaustive search of the space system. Since size grows exponentially with number processes, model techniques based on explicit enumeration can only handle relatively small examples. This phenomenon commonly called "State Explosion Problem". Over past ten years considerable progress has been made problem (1) representing symbolically using BDDs and (2) abstraction reduce that must be searched. As a result used successfully find extremely subtle errors in hardware controllers communication protocols. spite these successes, however, additional research needed large designs industrial complexity. aim paper give succinct survey symbolic introduce reader recent advances abstraction.