CTL model checking based on forward state traversal
Hiroaki Iwashita, Tsuneo Nakata, Fumiyasu Hirose · 1996
We present a CTL model checking algorithm based mainly on forward state traversal, which can check many realis-tic CTL properties without doing backward state traversal. This algorithm is effective in many situations where back-ward state traversal is more expensive than forward state traversal. We combine it with BDD-based state traversal techniques using partitioned transition relations. Experi-mental results show that our method can verify actual CTL properties of large industrial models which cannot be han-dled by conventional model checkers. 1