Learning to verify branching time properties

Abstract

We present a new model checking algorithm for verifying computation tree logic (CTL) properties. To our knowledge, this is the first CTL model checking algorithm for infinite state systems that can also handle fairness constraints. Our technique is based on using language inference to learn the fixpoints necessary for checking a CTL formula instead of computing them iteratively as is done in traditional model checking. This allows us to analyze infinite or large state-space systems where the traditional iterations may not converge or may take too long to converge. Our procedure is guaranteed to terminate with the correct answer if fixpoints needed for all subformulas of the CTL property are regular. We have extended our LEVER tool to use the technique presented in this paper and demonstrate its effectiveness by verifying a number of parametric and integer systems.