計算樹邏輯（CTL）是一種分支時間邏輯，意味著它的時間模型是一個樹狀結構，其中未來是不確定的；未來有不同的路徑，其中任何一條都可能是實現的實際路徑。它被用于軟件或硬件工件的形式化驗證，通常由被稱為模型檢查器的軟件應用程序來確定一個給定的工件是否擁有安全或活潑屬性。例如，CTL可以規定，當某些初始條件得到滿足時（例如，所有的程序變量都是正的，或者高速公路上沒有汽車跨越兩條車道），那么程序的所有可能的執行都會避免一些不理想的情況（例如，一個數字除以0或者兩輛車在高速公路上相撞）。在這個例子中，安全屬性可以由一個模型檢查器來驗證，該檢查器會探索所有可能的、滿足初始條件的程序狀態的轉換，并確保所有這些執行都滿足該屬性。計算樹邏輯屬于一類時間邏輯，包括線性時間邏輯（LTL）。盡管有些屬性只能在CTL中表達，有些屬性只能在LTL中表達，但在這兩種邏輯中可表達的所有屬性也都可以在CTL*中表達。

CTL的形式良好的公式語言是由以下語法生成的。CTL使用原子命題作為它的構建模塊，對系統的狀態進行陳述。然后，這些命題通過邏輯運算符和時間運算符被組合成公式。

邏輯操作符是常用的。?,∨,∧,?和?。除了這些運算符之外，CTL公式還可以使用布爾常數true和false。

時態運算符有以下幾種。路徑A上的量詞Φ-全部。Φ-全部：Φ必須在從當前狀態開始的所有路徑上成立。EΦ-存在：至少有一條從當前狀態開始的路徑上Φ成立。特定路徑的量詞Xφ-下一個：Φ必須在下一個狀態上成立（這個算子有時被稱為N而不是X）。Gφ-全局：φ在整個后續路徑上必須成立。Fφ-最后：φ最終必須成立（在后續路徑的某個地方）。φUψ-直到：φ必須至少成立，直到在某個位置ψ成立。這意味著ψ將在未來得到驗證。φWψ-弱的直到：φ必須持有，直到ψ持有。與U的區別是，不能保證ψ會被驗證。在CTL*中，時間運算符可以自由混合。在CTL中，算子必須總是分成兩組：一個路徑算子后面是一個狀態算子。請看下面的例子。CTL*在嚴格意義上比CTL更具表現力。

在CTL中，有最小的運算符集。所有的CTL公式都可以被轉換為只使用這些運算符。這在模型檢查中是很有用的。一個最小的運算符集是。{true,∨,?,EG,EU,EX}。一些用于時態運算符的轉換是。