Limbajul procesului temporal - Temporal Process Language

În informatică teoretică , Temporal Process Language (TPL) este un calcul al procesului care extinde CCS-ul lui Robin Milner cu noțiunea de sincronizare multi-party , care permite sincronizarea proceselor multiple pe un „ceas” global. Acest ceas măsoară timpul, deși nu în mod concret, ci mai degrabă ca un semnal abstract care definește când întregul proces poate merge mai departe.

Definiție informală

TPL este o extensie conservatoare a CCS, cu adăugarea unei acțiuni speciale numită σ care reprezintă trecerea timpului printr-un proces - bifarea unui ceas abstract. La fel ca în CCS, TPL prezintă prefixul de acțiune și poate fi descris ca fiind pacient , adică un proces va accepta în mod nepotrivit marcajul ceasului, scris ca ${\ displaystyle aP}$

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

Cheia utilizării timpului abstract este operatorul de timeout , care prezintă două procese, unul de a se comporta ca și când ceasul bifează, unul de a se comporta ca și cum nu se poate, adică

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

cu condiția ca procesul E să nu împiedice ceasul să bifeze.

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

cu condiția ca E să poată efectua acțiunea a de a deveni E '.

În TPL, există două modalități de a împiedica ceasul să bifeze. În primul rând prin prezența operatorului ω, de exemplu, în proces , ceasul este împiedicat să bifeze. Se poate spune că acțiunea a este insistentă , adică insistă să acționeze înainte ca ceasul să poată bifa din nou. ${\ displaystyle a.P + \ Omega}$

Al doilea mod în care poate fi prevenită bifarea este prin conceptul de progres-maxim , care afirmă că acțiunile tăcute (adică τ acțiuni) au întotdeauna prioritate și astfel suprimă acțiunile σ. Astfel, două procese paralele sunt capabile să se sincronizeze la un moment dat, nu este posibil ca ceasul să bifeze.

Astfel, un mod simplu de vizualizare a sincronizării multi-party este acela că un grup de procese compuse va permite trecerea timpului, cu condiția ca niciunul să nu îl împiedice, adică sistemul să fie de acord că este timpul să continuăm.

Definiție formală

Sintaxă

Fie un nume de acțiune care nu este tăcut, α orice nume de acțiune (inclusiv τ, acțiunea silențioasă) și X să fie o etichetă de proces utilizată pentru recurs.

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

Referințe

Matthew Hennessy și Tim Regan: o algebră de proces pentru sistemele de timp . Informații și calcul, 1995.