Learning to verify branching time properties

Abhay Vardhan, Mahesh Viswanathan

Research output: Contribution to conferencePaperpeer-review


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)
Number of pages4
StatePublished - 2005
Event20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005 - Long Beach, CA, United States
Duration: Nov 7 2005Nov 11 2005


Other20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005
Country/TerritoryUnited States
CityLong Beach, CA


  • CTL
  • Computational learning theory
  • Infinite state systems

ASJC Scopus subject areas

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


Dive into the research topics of 'Learning to verify branching time properties'. Together they form a unique fingerprint.

Cite this