Temporal Process Language - Temporal Process Language

I teoretisk informatikk er Temporal Process Language (TPL) en prosessberegning som utvider Robin Milners CCS med forestillingen om flerpartisynkronisering , som lar flere prosesser synkronisere på en global 'klokke'. Denne klokken måler tid, men ikke konkret, men snarere som et abstrakt signal som definerer når hele prosessen kan gå videre.

Uformell definisjon

TPL er en konservativ utvidelse av CCS, med tillegg av en spesiell handling kalt σ som representerer tidens gang med en prosess - avkrysningen av en abstrakt klokke. Som i CCS, har TPL handlingsprefiks, og det kan beskrives som å være tålmodig , det vil si at en prosess vil ta imot tikkingen av klokken, skrevet som ${\ displaystyle aP}$

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

Nøkkelen til bruken av abstrakt tid er timeout- operatøren, som presenterer to prosesser, en for å oppføre seg som om klokken tikker, en for å oppføre seg som om den ikke kan, dvs.

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

forutsatt prosess E forhindrer ikke at klokken tikker.

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

forutsatt at E kan utføre handling a for å bli E '.

I TPL er det to måter å forhindre at klokken tikker. Først er det via tilstedeværelsen av ω-operatøren, for eksempel i prosessen klokken hindres i å tikke inn. Det kan sies at handlingen a er insisterende , dvs. at den insisterer på å handle før klokken kan tikke igjen. ${\ displaystyle a.P + \ Omega}$

Den andre måten ticking kan forhindres på er via begrepet maksimal fremgang , som sier at stille handlinger (dvs. τ handlinger) alltid har forrang og dermed undertrykker σ handlinger. Således er to parallelle prosesser i stand til å synkronisere på et gitt tidspunkt, det er ikke mulig for klokken å krysse av.

Således er en enkel måte å se multisepartssynkronisering på at en gruppe sammensatte prosesser vil tillate tid å passere, forutsatt at ingen av dem forhindrer det, dvs. systemet er enig i at det er på tide å gå videre.

Formell definisjon

syntax

La a være et ikke-lydløst handlingsnavn, α være et hvilket som helst handlingsnavn (inkludert τ, den stille handlingen) og X være en prosessetikett som brukes til rekursjon.

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

referanser

Matthew Hennessy og Tim Regan: A Process Algebra for Timed Systems . Informasjon og beregning, 1995.