1996 Amir Pnueli —— 讓時間本身進入邏輯#

「程式會錯在『空間』（值算錯），也會錯在『時間』（順序、 響應、永遠等不到）。誰為後者發明了數學語言？」

案件檔案#

前因#

1977 年，Pnueli 在一封信件式論文《The Temporal Logic of Programs》中提出關鍵洞見。當時背景：反應式系統 （作業系統、通訊協定、控制系統）不斷與環境互動、永不 終止——Hoare 邏輯（1980 案）的「前條件→後條件」是為 終止程式設計的，對活體系統失效。

線索與推理#

線索一：時態邏輯作為規格語言#

Pnueli 引入哲學家 Prior 的時態邏輯（1957），把執行的 時間軸納入邏輯算子：

□P  永遠 P        ◇P  終將 P
○P  下一刻 P      P U Q  P 持續直到 Q 出現

安全性（safety）：□(P → ◇Q)？不，safety = □P（壞事永不發生）
活性（liveness）：◇P（好事終將發生）
典型規格：「請求後必獲回應」 = □(req → ◇ack)

正確性規格第一次可以用讀起來像英語句子的邏輯寫出， 且語義嚴格（Kripke 結構上的滿足）。

線索二：與模型檢查的會師（1981–）#

Clarke–Emerson 與 Queille–Sifakis（2007 案）獨立提出模型 檢查：窮舉有限狀態系統的所有狀態，自動判定規格是否 成立。時態邏輯（CTL/CTL*）成為其規格語言，模型檢查 成為其判定演算法——理論與工具在此閉環。

M ⊨ φ ？  （系統模型 M 是否滿足時態公式 φ）
反例自動生成：若不滿足，輸出違反 φ 的執行軌跡 ← 工業價值核心

線索三：狀態爆炸的對抗#

模型檢查的代價是指數級狀態空間。Pnueli 學派（與 Burch、 Clarke 等的 OBDD 符號方法、partial order reduction）持續 對抗——把「窮舉」變得可承受成為三十年戰役。

線索四：實時擴張（MTL/TLPTL）#

「在 100ms 內必須回應」——把實時約束加入時態邏輯， 直接服務於嵌入式與安全關鍵系統（汽車、航太 DO-178C）。

理論評析#

時態邏輯的偵探學意義：把「執行歷史」當作調查對象。 命令式驗證看程式碼（靜態），時態邏輯看軌跡（動態）—— 錯誤的形態從「算錯」擴展到「時序違約」：死結、活結、 飢餓、雙花（分佈式），全部可被統一陳述。

後果#

• 工業驗證：SPIN（響星能力者，用於計畫協定）、NuSMV、 CBMC；晶片設計的 assertion-based verification 已是 標準流程。
• 自動駕駛與機器人的 runtime verification 正在重演此案。

關聯案件#

→ 2007-Clarke-Emerson-Sifakis與模型檢查、1991-Robin-Milner與ML型別系統及CCS、1980-C.A.R.-Hoare與程式語言理論及CSP