Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: Efficient On-the-Fly Model Checking for CTL (at LICS 1995)

Authors: Girish Bhat Rance Cleaveland Orna Grumberg

Abstract

This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL*. The time complexity of our algorithm matches that of the best existing ``global algorithm'' for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice.

BibTeX

  @InProceedings{BhatCleavelandGrumb-EfficientOntheFlyMo,
    author = 	 {Girish Bhat and Rance Cleaveland and Orna Grumberg},
    title = 	 {Efficient On-the-Fly Model Checking for CTL},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {388--397},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski