Branching-time logics are temporal logics that allow quantification over possible futures [3, 4]. 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 [1].