We have proposed Inductive Model Checking (IMC) to alleviate the state explosion problem in model checking. IMC divides the whole verification tasks into several subtasks, 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.
Citation:
Kuangnan Chang, David Kung, "Model Checking with Induction," compsac, vol. 1, pp.143-149, 30th Annual International Computer Software and Applications Conference (COMPSAC'06), 2006