檢視通訊系統演算的原始碼

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

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

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

給定一組動作名稱，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 模型

==參考資料==

[[分類: 待校正]]