跳至內容

通訊系統演算

出自Taiwan Tongues 繁中維基
於 2025年9月25日 (四) 19:36 由 TaiwanTonguesApiRobot留言 | 貢獻 所做的修訂 (從 JSON 檔案批量匯入)

(差異) ←上個修訂 | 已批准修訂 (差異) | 最新修訂 (差異) | 下個修訂→ (差異)

溝通系統演算(calculus of communicating systems,簡稱 CCS)是羅賓·米爾納於 1980 年左右提出的一種程序演算,也是一本描述該演算的書名。其動作模型化了恰好兩個參與者之間不可分割的通訊。該形式語言包含用以描述並行組合、動作間的加法以及範疇限制的基元。CCS 可用於評估系統屬性(如死鎖或活鎖)的定性正確性。

根據米爾納的說法:「儘管我們在選擇基本組合子時非常注重精簡,但這些選擇並無標準可言。我們演算的特點不在於組合子的精確選擇,而在於其詮釋和數學框架的選擇。」

此語言的表達式被詮釋為一個標記轉移系統。在這些模型之間,互模擬被用作一種語義等價性。

語法

給定一組動作名稱,CCS 程序的集合由以下 BNF 文法定義:

<math>P ::= 0\,\,\, | \,\,\,a.P_1\,\,\, | \,\,\,A\,\,\, | \,\,\,P_1+P_2\,\,\, | \,\,\,P_1|P_2\,\,\, | \,\,\,P_1[b/a]\,\,\, | \,\,\,P_1{\backslash}a\,\,\,</math>

語法的各部分,按上列順序說明如下:

不活動程序:不活動程序 <math>0</math> 是一個有效的 CCS 程序
動作:程序 <math>a.P_1</math> 可以執行一個動作 <math>a</math>,然後繼續作為程序 <math>P_1</math>
程序識別碼:寫作 <math>A \overset{\underset{\mathrm{def}}{}}{=} P_1</math> 來使用識別碼 <math>A</math> 代表程序 <math>P_1</math>(<math>P_1</math> 本身可能包含識別碼 <math>A</math>,即允許遞迴定義)
加法:程序 <math>P_1+P_2</math> 的行為可能像程序 <math>P_1</math> 或程序 <math>P_2</math>
並行組合:<math>P_1|P_2</math> 表示程序 <math>P_1</math> 和 <math>P_2</math> 同時存在
重命名:<math>P_1[b/a]</math> 是將程序 <math>P_1</math> 中所有名為 <math>a</math> 的動作重命名為 <math>b</math> 的程序
限制:<math>P_1{\backslash}a</math> 是程序 <math>P_1</math> 中排除動作 <math>a</math> 後的程序

相關演算、模型與語言

  • 通訊順序程序(Communicating sequential processes,簡稱 CSP),由東尼·霍爾開發,是一個與 CCS 同時期出現的形式語言。
  • 通訊程序代數(The Algebra of Communicating Processes,簡稱 ACP)由 Jan Bergstra 和 Jan Willem Klop 於 1982 年開發,它使用公理化方法(採泛代數風格)來推論與 CCS 類似的程序類別。
  • π-演算(pi-calculus)由羅賓·米爾納、Joachim Parrow 和 David Walker 於 80 年代末期開發,它透過允許程序通訊通道本身的名稱,以通訊連結的流動性擴展了 CCS。
  • PEPA,由 Jane Hillston 開發,引入了以指數分佈率和機率選擇表示的活動時序,從而可以評估效能指標。
  • 可逆通訊並行系統(Reversible Communicating Concurrent Systems,簡稱 RCCS)由 Vincent Danos、Jean Krivine 及其他人提出,為 CCS 程序的執行引入了(部分)可逆性。

其他一些基於 CCS 的語言:

  • 廣播系統演算
  • 時間序列規範語言(Language Of Temporal Ordering Specification,簡稱 LOTOS)
  • 空間顯式生態模型之程序演算(Process Calculus for Spatially-Explicit Ecological Models,簡稱 PALPS)是 CCS 的一個擴展,增加了機率選擇、位置以及位置屬性
  • Java 編排語言直譯器引擎(Java Orchestration Language Interpreter Engine,簡稱 Jolie)

用於研究類 CCS 系統的模型:

  • 歷史么半群
  • Actor 模型

參考資料