時間的プロセス言語

理論計算機科学において、Temporal Process Language (TPL) は、Robin Milner のCCS をマルチパーティ同期の概念で拡張したプロセス計算であり、これにより複数のプロセスがグローバル「クロック」で同期できるようになります。このクロックは時間を測定しますが、具体的なものではなく、プロセス全体がいつ前進できるかを定義する抽象的な信号として測定します。

TPLはCCSの保守的な拡張であり、プロセスの時間の経過を表すσと呼ばれる特別なアクション（抽象的な時計の刻み）が追加されています。CCSと同様に、TPLはアクションの接頭辞を特徴としており、忍耐強いと表現できます。つまり、プロセスは時計の刻みを黙って受け入れます。次のように記述されます。 ${\displaystyle aP}$

${\displaystyle aP\rightarrow ^{a}aP}$

抽象時間の使用の鍵となるのはタイムアウト演算子であり、これは2つのプロセスを提示します。1つは時計が刻んでいるかのように動作し、もう1つは時計が刻んでいないかのように動作します。

${\displaystyle \lfloor E\rfloor (F)\rightarrow ^{\sigma }F}$

ただし、プロセス E がクロックの進行を妨げない場合に限ります。

${\displaystyle \lfloor E\rfloor (F)\rightarrow ^{\sigma }E'}$

ただし、E がアクション a を実行して E' になることができる場合。

TPL では、クロックの刻みを止める方法が 2 つあります。1 つ目は、ω 演算子を使用することです。たとえば、プロセスではクロックの刻みが止められます。アクション a は、クロックが再び刻み始める前に必ず動作することを要求している、つまり、執拗であると言えます。 ${\displaystyle a.P+\Omega }$

刻みを止める 2 つ目の方法は、最大進行の概念を利用することです。これは、サイレント アクション (つまり、τ アクション) が常に σ アクションよりも優先され、σ アクションを抑制するというものです。したがって、2 つの並列プロセスが特定の瞬間に同期できる場合、時計が刻み続けることはできません。

したがって、マルチパーティ同期を簡単に見る方法は、構成されたプロセスのグループが、いずれのプロセスもそれを妨げない限り、つまりシステムが次に進む時間であると同意しない限り、時間の経過を許可するというものです。

a を非サイレントアクション名、α を任意のアクション名（サイレントアクション τ を含む）、X を再帰に使用されるプロセスラベルとします。

${\displaystyle {\begin{matrix}Proc::=&\alpha .Proc\\|&\lfloor Proc\rfloor (Proc)\\|&Proc+Proc\\|&Proc\;|\;Proc\\|&recX.Proc\\|&X\\|&\Omega \\|&Proc\setminus a\\|&0\\\end{matrix}}}$

Matthew Hennessyと Tim Regan :時間制限付きシステムのためのプロセス代数。Information and Computation、1995 年。