Learning to verify branching time properties

Abhay Vardhan, Mahesh Viswanathan

Research output: Contribution to conferencePaper

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.

Original languageEnglish (US)
Pages325-328
Number of pages4
DOIs
StatePublished - Dec 1 2005
Event20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005 - Long Beach, CA, United States
Duration: Nov 7 2005Nov 11 2005

Other

Other20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005
CountryUnited States
CityLong Beach, CA
Period11/7/0511/11/05

    Fingerprint

Keywords

  • CTL
  • Computational learning theory
  • Infinite state systems

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Human-Computer Interaction
  • Software

Cite this

Vardhan, A., & Viswanathan, M. (2005). Learning to verify branching time properties. 325-328. Paper presented at 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005, Long Beach, CA, United States. https://doi.org/10.1145/1101908.1101961