Lógica del Árbol de Computación (CTL)

Una lógica temporal de tiempo ramificado que combina operadores temporales con cuantificadores de caminos explícitos (A para 'para todos los caminos', E para 'existe un camino') para expresar propiedades sobre árboles de futuros posibles más que sobre líneas temporales individuales.