Efficient on-the-fly model checking for CTL

TitleEfficient on-the-fly model checking for CTL
Publication TypeConference Papers
Year of Publication1995
AuthorsBhat G, Cleaveland R, Grumberg O
Conference Name, Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings
Date Published1995/06/26/29
ISBN Number0-8186-7050-9
KeywordsAlgorithm design and analysis, Automata, computational complexity, Computer science, CTL, Encoding, finite automata, finite-state system, global algorithm, Logic, LTL, on-the-fly model checking, Performance analysis, Safety, State-space methods, sublogic, temporal logic, time complexity

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