Model Checking with Induction

We have proposed inductive model checking (IMC) to alleviate the state explosion problem in model checking. IMC divides the whole verification tasks into several sub-tasks, and applies the three inductive steps (basis, hypothesis, and induction) to verify a system with model checking. In this paper, we continue our research by determining those temporal formulas, namely, persistent temporal formulas, which are verifiable with IMC. One important characteristic of a persistent temporal formula is that it contains a periodic temporal formula that must be held persistently. From the verification results of the periodic formula with different sequences of states, IMC concludes the verification of the persistent temporal formula