CTL staat voor Computation Tree Logic. Het is een formele taal die wordt gebruikt om logische formules te schrijven die gebruikt kunnen worden om systemen te beschrijven en te analyseren. Het is een taal die gebaseerd is op de logica van binaire bomen, waarbij elke knoop een logische operatie bevat. CTL wordt gebruikt in veel verschillende gebieden, waaronder software engineering, formele verificatie en modelchecking.