Язык логики ветвящегося времени CTL (compu­tational tree logic) – удобное и эффективное средство для описания свойств различных сложных вычислительных систем, в том числе с целью их последующей верификации [1, 2]. Его существенным отличием от хорошо известного и широко используемого языка логики предикатов QCL является то, что важные для прикладного аспекта задачи общезначимости и выполнимости CTL-формул разрешимы [3], в то время как для проблем тождественной истинности и выполнимости формул языка логики QCL разрешающей процедуры не существует в принципе [4].

Оба языка позволяют описывать свойства (серийного) бинарного отношения: свойства отношения достижимости в шкалах Крипке для CTL, с одной стороны, могут быть описаны с помощью модальностей языка CTL, а с другой – с помощью формул языка логики предикатов, содержащих предикатную букву