Philippe Schnoebelen, Laboratory for Specification and Verification, ENS, Cachan
In the early eighties, several extensions of CTL have been proposed (mostly by Emerson and Halpern) with the aim of repairing some deficiencies in the expressive power of CTL, but without going all the way to CTL* where model checking is PSPACE-complete.
For these logics lying between CTL and CTL*, the precise complexity of the model checking problem has only been recently characterized (Schnoebelen et al., in FoSSaCS 2001 and ICALP 2003). We present these recent results.
The model checking problems for these branching-time logics share a similar structure, and their solution involve bounded invocations of NP oracles, with different logics requiring different bounds. The main difficulty with this work is that it requires investigating complexity classes that are very rarely encountered in computer science.