行為時序邏輯（The Temporal Logic of Actions）是由萊斯利·蘭伯特（Leslie Lamport）發展的用於規範和推理並發自反應系統的時間邏輯。 主要套用於計算機科學，程式驗證。
基本介紹
- 中文名：行為時序邏輯
- 外文名：The Temporal Logic of Actions
簡介,萊斯利·蘭波特,計算機科學,
簡介
行為時序邏輯（The Temporal Logic of Actions）是由萊斯利·蘭伯特（Leslie Lamport）發展的用於規範和推理並發自反應系統的時間邏輯。 主要套用於計算機科學，程式驗證。
萊斯利·蘭波特
萊斯利·蘭波特（英語：Leslie Lamport，1941年2月7日－），美國計算機科學家。也是排版系統LaTeX的開發者。
蘭波特1941年出生於紐約，是歐洲移民的兒子。 在麻省理工學院獲學士學位以後，蘭波特到布蘭代斯大學攻讀數學博士，不久後放棄，到佛蒙特州一所小型文科學校——萬寶路學院教授數學。之後到麻省計算機協會做兼職工作，做ILLIAC設計。
1972年獲博士學位，繼續研究ILLIAC。蘭波特最終得出證明，分布系統中的相對次序與觀察者有關。
2013年，萊斯利·蘭波特獲圖靈獎。
計算機科學
計算機科學（英語：computer science，有時縮寫為CS）是系統性研究信息與計算的理論基礎以及它們在計算機系統中如何實現與套用的實用技術的學科。它通常被形容為對那些創造、描述以及轉換信息的算法處理的系統研究。計算機科學包含很多分支領域；有些強調特定結果的計算，比如計算機圖形學；而有些是探討計算問題的性質，比如計算複雜性理論；還有一些領域專注於怎樣實現計算，比如程式語言理論是研究描述計算的方法，而程式設計是套用特定的程式語言解決特定的計算問題，人機互動則是專注於怎樣使計算機和計算變得有用、好用，以及隨時隨地為人所用。
有時公眾會誤以為計算機科學就是解決計算機問題的事業（比如信息技術），或者只是與使用計算機的經驗有關，如玩遊戲、上網或者文字處理。其實計算機科學所關注的，不僅僅是去理解實現類似遊戲、瀏覽器這些軟體的程式的性質，更要通過現有的知識創造新的程式或者改進已有的程式。
