Язык темпорального процесса - Temporal Process Language

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

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

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

${\ Displaystyle AP \ rightarrow ^ {a} AP}$

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

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

при условии, что процесс E не предотвращает тиканье часов.

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

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

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

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

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

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

Синтаксис

Пусть 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}}}$

Ссылки

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