This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
10th Annual IEEE Symposium on Logic in Computer Science (LICS'95)
Efficient On-the-Fly Model Checking for CTL
San Diego, California
June 26-June 29
ISBN: 0-8186-7050-6
ASCII Text
x 
 
Girish Bhat, Rance Cleaveland, Orna Grumberg, "Efficient On-the-Fly Model Checking for CTL," Logic in Computer Science, Symposium on, pp. 388, 10th Annual IEEE Symposium on Logic in Computer Science (LICS'95), 1995.
 
 
BibTex
x
 
@article{ 10.1109/LICS.1995.523273,
author = {Girish Bhat and Rance Cleaveland and Orna Grumberg},
title = {Efficient On-the-Fly Model Checking for CTL},
journal ={Logic in Computer Science, Symposium on},
volume = {0},
year = {1995},
issn = {1043-6871},
pages = {388},
doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.1995.523273},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Logic in Computer Science, Symposium on
TI - Efficient On-the-Fly Model Checking for CTL
SN - 1043-6871
SP
EP
A1 - Girish Bhat,
A1 - Rance Cleaveland,
A1 - Orna Grumberg,
PY - 1995
KW - Model checking
KW - temporal logic
KW - program verification
KW - formal methods
VL - 0
JA - Logic in Computer Science, Symposium on
ER -
 
Girish Bhat, Department of Computer Science, North Carolina State University, Raleigh, NC
Rance Cleaveland, Department of Computer Science, North Carolina State University, Raleigh, NC
Orna Grumberg, Department of Computer Science, The Technion, Haifa, ISRAEL
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.
Index Terms:
Model checking, temporal logic, program verification, formal methods
Citation:
Girish Bhat, Rance Cleaveland, Orna Grumberg, "Efficient On-the-Fly Model Checking for CTL," lics, pp.388, 10th Annual IEEE Symposium on Logic in Computer Science (LICS'95), 1995
Usage of this product signifies your acceptance of the Terms of Use.