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

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

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

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

${displaystyle a.Pightarrow ^ {a} a.P}$

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

${displaystyle lfloor Efloor (F) ightarrow ^ {sigma} F}$

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

${displaystyle lfloor Efloor (F) ightarrow ^ {sigma} E '}$

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

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

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

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

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

Синтаксис

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

${displaystyle {egin {matrix} Proc :: = & alpha .Proc | & lfloor Procfloor (Proc) | & Proc + Proc | & Proc; |; Proc | & recX.Proc | & X | & Omega | & Procsetminus a | & 0 end {matrix}}}$

Рекомендации

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