時間的プロセス言語

理論計算機科学において、時間プロセス言語（TPL）は、ロビン・ミルナーのCCSをマルチパーティ同期の概念で拡張したプロセス計算法です。マルチパーティ同期により、複数のプロセスがグローバルな「クロック」に基づいて同期することが可能になります。このクロックは時間を計測しますが、具体的なものではなく、プロセス全体がいつ前進できるかを定義する抽象的な信号として機能します。

非公式な定義

TPLはCCSの保守的な拡張であり、プロセスによる時間の経過、つまり抽象的な時計の刻みを表すσと呼ばれる特別な動作が追加されています。CCSと同様に、TPLは動作接頭辞を備えており、忍耐強い（patient）状態と表現できます。つまり、プロセスは時計の刻みを無為に受け入れるということです。これは次のように表されます。 ${\displaystyle aP}$

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

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

${\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}}}$

参考文献

マシュー・ヘネシー、ティム・リーガン：「時間制限付きシステムのためのプロセス代数」Information and Computation、1995年。