Title :
Model Checking Branching Time Logics
Author_Institution :
CNRS, Cachan
Abstract :
Branching-time logics are temporal logics that allow quantification over possible futures. Such logics have been considered very early by the automated verification community because efficient model-checking algorithms for logics like CTL could be easily implemented and were used successfully.
Keywords :
computational complexity; formal verification; temporal logic; CTL; NP-complete problem; NP-hard problem; automated verification community; branching-time logic; model-checking algorithm; temporal logic; Automata; Automatic logic units; Automatic programming; Circuits; Computer science; Educational institutions; Logic programming; Polynomials; Power system modeling;
Conference_Titel :
Temporal Representation and Reasoning, 14th International Symposium on
Conference_Location :
Alicante
Print_ISBN :
978-0-7695-2836-6
DOI :
10.1109/TIME.2007.52
