時序邏輯（temporal logic）
一般的邏輯談的是什麼為真，就這樣。但當你對一個運行中的程式或協定進行推理時，真值會隨時間改變：鎖現在被持有、稍後被釋放；請求終究會被回應；錯誤絕不可發生。時序邏輯是把邏輯加上談論時間的運算子後的擴充——談論現在、下一步、永遠、終究會成立什麼——讓你能寫下關於系統運行時行為的精確陳述。
它在一般命題之上添加少數幾個時序運算子。在常見的線性時間版本（LTL）裡，沿著一個無窮的狀態序列閱讀，關鍵運算子是：G p（「全域地」，p 在每個未來時刻都成立——一個像「絕不當機」的安全性主張）、F p（「終究」或最終，p 在某個未來時刻成立——一個像「終究會回應」的活性主張）、X p（「下一步」，p 在緊接的下一步成立），以及 p U q（「直到」，p 持續成立直到 q 變為真）。它們可組合：G F p 讀作「無窮多次 p」（永遠地，終究，p 再度成立），正是 Buchi 自動機所接受的型態；G（請求蘊含 F 回應）說「每個請求終究被回應」。每個公式描述一組可接受的無窮行為。
時序邏輯是形式驗證的規格語言。工程師把硬體與軟體所期望的性質——互斥、無死結、終究會送達——陳述成時序公式，模型檢驗器再證明系統滿足它們，或交回一條反例軌跡。讓這件事得以自動化的環節，正是與 Buchi 自動機的連結：一個 LTL 公式可被編譯成一個恰好接受所有滿足它之執行的 Buchi 自動機，把一個邏輯問題化為一個自動機問題。存在不同的時序邏輯（LTL 是線性的，CTL 是分支的，區分「在所有未來上」與「在某個未來上」），各有自己的表達力與權衡。
互斥的安全性性質「兩個行程絕不同時處於各自的臨界區」就是 LTL 公式 G not(crit1 and crit2)：全域地、在每一步，從不發生兩者皆在臨界區。其活性的搭檔「想要鎖的行程終究會得到它」則是 G (want1 implies F crit1)。
時序運算子（永遠 G、終究 F、下一步 X、直到 U）陳述真值必須如何隨時間演變。
「終究」（F）並不是指「在固定步數之內」——它只承諾某個未指定的未來時刻。而線性時間（LTL）與分支時間（CTL）邏輯確實不同：彼此都無法表達對方所能表達的一切，所以選擇哪一個會影響你能陳述哪些性質。