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.

REFERENCES

• 1: R. Alur, P. Madhusudan, and W. Nam. Symbolic compositional verification by learning assumptions. In Computer Aided Verification, 2005.
• 2: Dana Angluin, Learning regular sets from queries and counterexamples, Information and Computation, v.75 n.2, p.87-106, November 1, 1987 [doi>10.1016/0890-5401(87)90052-6]
• 3: S. Bardin, A. Finkel, and J. Leroux. FASTer acceleration of counter automata in practice. In TACAS, 2004.
• 4: C. Bartzis and T. Bultan. Widening arithmetic automata. In Computer Aided Verification, 2004.
• 5: Tevfik Bultan , Tuba Yavuz-Kahveci, Action Language Verifier, Proceedings of the 16th IEEE international conference on Automated software engineering, p.382, November 26-29, 2001
• 6: E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. The MIT Press, 2000.
• 7: FAST. Fast acceleration of symbolic transition systems. http://www.lsv.ens-cachan.fr/fast/, 2004.
• 8: P. Habermehl and T. Vojnar. Regular model checking using inference of regular languages. In Proc. of Infinity'04, London, UK, 2004.
• 9: Michael J. Kearns , Umesh V. Vazirani, An introduction to computational learning theory, MIT Press, Cambridge, MA, 1994
• 10: LEVER. Learning to verify tool. http://osl.cs.uiuc.edu/~vardhan/lever.html, 2004.
• 11: Ronald L. Rivest , Robert E. Schapire, Inference of finite automata using homing sequences, Information and Computation, v.103 n.2, p.299-347, April 1993 [doi>10.1006/inco.1993.1021 ]
• 12: T. Touili. Regular model checking using widening techniques. In ENTCS, volume 50. Elsevier, 2001.
• 13: A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Actively learning to verify safety for FIFO automata. In LNCS 3328, Proc. of FSTTCS'04, pages 494--505, 2004.
• 14: A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Using language inference to verify omega-regular properties. In TACAS, 2005.
• 15: A. Vardhan and M. Viswanathan. Learning to verify branching time properties. TR UIUCDCS-R-2005-2630, http://osl.cs.uiuc.edu/docs/ctlLearn/ctlLearnTR.pdf, Computer Science, University of Illinois, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Verification

Keywords:
CTL, computational learning theory, infinite state systems