Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Learning to verify branching time properties

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We present a new model checking algorithm for verifying computation tree logic (CTL) properties. 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. We allow fairness constraints to be specified for verification of various liveness properties. The main challenge in developing a learning based model checking algorithm for CTL is that CTL properties express nested fixpoints. We overcome this challenge by developing a new characterization of CTL properties in terms of functions that have unique fixpoints. We instantiate our technique to systems in which states are encoded as strings and use a regular inference algorithm to learn the CTL fixpoints. We prove that if the fixpoints have a regular representation, our procedure will always terminate with the correct answer. 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. 1. Abdulla PA, Jonsson B, Nilsson M, d'Orso J (2003) Algorithmic improvements in regular model checking. In: Computer-Aided verification (CAV′03), LNCS, vol 2725, Springer, pp 236–248

  2. 2. Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: 2nd ACM SIGPLAN-SIGACT symposium on principles of program languages

  3. 3. Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of the 17th international conference on computer aided verification

  4. 4. ALV (2004) Action language verifier. http://www.cs.ucsb.edu/~bultan/composite/

  5. 5. Ammons G, Bodík R, Larus JR (2002) Mining specifications. ACM SIGPLAN Notices 37(1):4–16

    Article  Google Scholar 

  6. 6. Angluin D (1987) Learning regular sets from queries and counterexamples. Inform Comput 75(2):87–106

    Article  MATH  MathSciNet  Google Scholar 

  7. 7. Annichini A, Bouajjani A, Sighireanu M (2001) TReX: a tool for reachability analysis of complex systems. In: Berry G, Comon H, Finkel A (eds) Proceedings of the international conference on computer aided verification (CAV′01), lecture notes in computer science, vol 1855, Springer, Paris, France

    Google Scholar 

  8. 8. Bardin S, Finkel A, Leroux J (2004) FASTer acceleration of counter automata in practice. In: Jensen K, Podelski A (eds) Proceedings of the 10th international conference on tools and algorithms for construction and analysis of systems (TACAS′04), lecture notes in computer science, vol 2988. Springer, Barcelona, Spain, pp 576–590

    Google Scholar 

  9. 9. Bartzis C, Bultan T (2004) Widening arithmetic automata. In: Computer aided verification, 2004

  10. 10. Berstel J (1979) Transductions and context-free-languages. B.G. Teubner, Stuttgart

    MATH  Google Scholar 

  11. 11. Boigelot B (1999) Symbolic methods for exploring infinite state spaces. PhD thesis, Collection des Publications de la Faculté des Sciences Appliquées de l'Université de Liége

  12. 12. Boigelot B, Legay A, Wolper P (2003) Iterating transducers in the large (extended abstract). In: CAV: International conference on computer aided verification

  13. 13. Bouajjani A, Jonsson B, Nilsson M, Touili T (2000) Regular model checking. In: Emerson EA, Sistla AP (eds) Proceedings of the 12th International Conference on Computer-Aided Verification (CAV′00), LNCS, vol 1855, Springer, pp 403–418

  14. 14. Bultan T (1998) Automated symbolic analysis of reactive systems. PhD thesis, Department of Computer Science, University of Maryland, College Park, MD

  15. 15. Bultan T, Gerber R, Pugh W (1997) Symbolic model checking of infinite state programs using presburger arithmetic. In: Proceedings of the 9th international conference on computer aided verification (CAV 1997). pp 400–411

  16. 16. Bultan T, Yavuz-Kahveci T (2001) Action language verifier. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, pp 382–386

  17. 17. Clarke E, Chaki S, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Proceedings of the 17th International Conference on Computer Aided Verification

  18. 18. Clarke EM, Grumberg O, Peled DA (2000) Model checking. Number ISBN:0262032708. The MIT Press

  19. 19. Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp 331–346

  20. 20. Delzanno G, Podelski A (1999) Model checking in CLP, LNCS 1579:223–239

    Google Scholar 

  21. 21. FAST (2004) Fast acceleration of symbolic transition systems. http://www.lsv.ens-cachan.fr/fast/

  22. 22. Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere! Theor Comput Sci 256(1–2):63–92

    Article  MATH  MathSciNet  Google Scholar 

  23. 23. Habermehl P, Vojnar T (2004) Regular model checking using inference of regular languages. In: Proceedings of infinity′04, London, UK

  24. 24. Hopcroft JE, Motwani R, Rotwani, Ullman JD (2000) Introduction to automata theory, languages and computability. Addison-Wesley Longman Publishing Co Inc

  25. 25. Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. The MIT Press, Cambridge, Massachusetts

    Google Scholar 

  26. 26. Klarlund N, Møller A (2004) Mona. http://www.brics.dk/mona/

  27. 27. Kleene S (1952) Introduction to metamathematics. D. van Nostrand, Princeton

    MATH  Google Scholar 

  28. 28. LASH (2004) The liege automata-based symbolic handler. http://www.montefiore.ulg.ac.be/~boigelot/ research/lash/

  29. 29. LEVER (2004) Learning to verify tool. http://www.montefiore.ulg.ac.be/~boigelot/ research/lash/http://osl.cs.uiuc.edu/ vardhan/lever.html

  30. 30. Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inform Comput 103(2):299–347

    Article  MATH  MathSciNet  Google Scholar 

  31. 31. Rybina T, Voronkov A (2002) Brain: backward reachability analysis with integers. In: AMAST, pp 489–494

  32. 32. Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2):285–309

    MATH  MathSciNet  Google Scholar 

  33. 33. Touili T (2001) Regular model checking using widening techniques. In: ENTCS, vol 50. Elsevier

  34. 34. Vardhan A (2006) Learning to verify systems. PhD thesis, Department of Computer Science, University of Illinois at Urbana Champaign

  35. 35. Vardhan A, Sen K, Viswanathan M, Agha G (2004) Actively learning to verify safety for FIFO automata. In: LNCS 3328, Proceedings of FSTTCS′04, Chennai, India, pp 494–505

  36. 36. Vardhan A, Sen K, Viswanathan M, Agha G (2004) Learning to verify safety properties. In: LNCS 3308, Proceedings of ICFEM′04, Seattle, USA, pp 274–288

  37. 37. Vardhan A, Sen K, Viswanathan M, Agha G (2005) Using language inference to verify omega-regular properties. In: Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS′05), vol 3440, Springer, Edinburgh, UK, pp 45–60

    Google Scholar 

  38. 38. Vardhan A, Viswanathan M (2005) Learning to verify branching time properties. In: Proceedings of the twentieth IEEE/ACM International Conference on Automated Software Engineering. Long Beach, California, USA

Download references

Author information

Authors and Affiliations

  1. Google, Inc., Urbana, Illinois

    Abhay Vardhan

  2. Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, Urbana, USA

    Mahesh Viswanathan

Authors
  1. Abhay Vardhan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mahesh Viswanathan
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

A preliminary version of this work appeared in the proceedings of the twentieth IEEE/ACM International conference on Automated Software Engineering, Long Beach, California, USA, 2005.

Part of the work was done when the first author was at the University of Illinois.

Supported in part by DARPA/AFOSR MURI Award F49620-02-1-0325 and NSF 04-29639.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Vardhan, A., Viswanathan, M. Learning to verify branching time properties. Form Methods Syst Des 31, 35–61 (2007). https://doi.org/10.1007/s10703-006-0026-x

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0026-x

Keywords

Search

Navigation