Logika CTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.
- w porównaniu do logiki CTL*, każdy operator temopralny musi być poprzedzony przez operator ścieżkowy ( bądź ):
- formuła poprawna zarówno w CTL*, jak i w CTL:
- formuła poprawna w CTL*, ale niepoprawna w CTL:
- każda taka para operatorów: tworzy operator logiki CTL.
- operatory są podstawowe, a z nich można wyprowadzić pozostałe:
- – formuła jest prawdziwa w strukturze w stanie
- warunki prawdziwości podstawowych formuł: