Язык временных процессов

В информатике теоретической язык временных процессов (TPL) представляет собой исчисление процессов , которое расширяет Робина Милнера CCS понятием многосторонней синхронизации , которая позволяет синхронизировать несколько процессов по глобальным «часам». Эти часы измеряют время, но не конкретно, а скорее как абстрактный сигнал, определяющий, когда весь процесс может двигаться дальше.

Неформальное определение

TPL — это консервативное расширение CCS с добавлением специального действия, называемого σ, представляющего ход времени процессом — тиканье абстрактных часов. Как и в CCS, TPL имеет префикс действия, и его можно описать как терпеливый , то есть процесс. $a.P$ будет праздно принимать тиканье часов, написанное как

$a.P\rightarrow ^{a}a.P$

Ключом к использованию абстрактного времени является оператор тайм-аута , который представляет два процесса: один ведет себя так, как будто часы тикают, а другой ведет себя так, как будто он не может этого сделать, т.е.

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

при условии, что процесс E не мешает тиканию часов.

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

при условии, что E может выполнить действие a, чтобы стать E'.

В TPL есть два способа предотвратить тиканье часов. Во-первых, благодаря наличию оператора ω, например, в процессе $a.P+\Omega$ часы не тикают. Можно сказать, что действие a настойчиво , т. е. оно настаивает на действии до того, как часы снова начнут тикать.

Второй способ предотвращения тиканья — это концепция максимального прогресса , которая гласит, что молчаливые действия (т. е. действия τ) всегда имеют приоритет над действиями σ и, таким образом, подавляют их. Таким образом, если два параллельных процесса могут синхронизироваться в данный момент, часы не могут тикать.

Таким образом, простой способ рассматривать многостороннюю синхронизацию состоит в том, что группа составленных процессов позволяет пройти времени при условии, что ни один из них не препятствует этому, т. е. система согласна, что пришло время двигаться дальше.

Формальное определение

Синтаксис

Пусть a — имя не-тихого действия, α — любое имя действия (включая τ, молчаливое действие), а X — метка процесса, используемая для рекурсии.

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

Ссылки

Мэтью Хеннесси и Тим Риган: Алгебра процессов для временных систем . Информация и вычисления, 1995.