Lenguaje de proceso temporal - Temporal Process Language

En informática teórica , el lenguaje de proceso temporal (TPL) es un cálculo de procesos que amplía el CCS de Robin Milner con la noción de sincronización multipartita , que permite que varios procesos se sincronicen en un 'reloj' global. Este reloj mide el tiempo, aunque no de forma concreta, sino como una señal abstracta que define cuándo puede avanzar todo el proceso.

Definición informal

TPL es una extensión conservadora de CCS, con la adición de una acción especial llamada σ que representa el paso del tiempo por un proceso: el tic-tac de un reloj abstracto. Como en CCS, TPL presenta un prefijo de acción y se puede describir como paciente , es decir, un proceso aceptará ociosamente el tic-tac del reloj, escrito como ${\ Displaystyle AP}$

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

La clave para el uso del tiempo abstracto es el operador de tiempo de espera , que presenta dos procesos, uno para comportarse como si el reloj marcara y otro para comportarse como si no pudiera, es decir

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

siempre que el proceso E no impida el tic-tac del reloj.

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

siempre que E pueda realizar la acción a para convertirse en E '.

En TPL, hay dos formas de evitar que el reloj corra. Primero es a través de la presencia del operador ω, por ejemplo, en el proceso, se evita que el reloj corra. Se puede decir que la acción a es insistente , es decir, insiste en actuar antes de que el reloj vuelva a marcar. ${\ Displaystyle a.P + \ Omega}$

La segunda forma en que se puede prevenir el tic-tac es a través del concepto de progreso máximo , que establece que las acciones silenciosas (es decir, las acciones τ) siempre tienen prioridad sobre las acciones σ y, por lo tanto, las suprimen. Por lo tanto, si dos procesos paralelos son capaces de sincronizarse en un instante dado, no es posible que el reloj marque.

Por lo tanto, una forma sencilla de ver la sincronización multipartita es que un grupo de procesos compuestos permitirá que pase el tiempo siempre que ninguno de ellos lo impida, es decir, el sistema acepta que es hora de seguir adelante.

Definicion formal

Sintaxis

Sea a un nombre de acción no silencioso, α sea cualquier nombre de acción (incluido τ, la acción silenciosa) y X sea una etiqueta de proceso utilizada para la recursividad.

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

Referencias

Matthew Hennessy y Tim Regan: un álgebra de procesos para sistemas cronometrados . Información y Computación, 1995.