
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
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
