Lenguaje de procesos temporales

En informática teórica , el Lenguaje de Procesos Temporales (TPL) es un cálculo de procesos que extiende el CCS de Robin Milner con la noción de sincronización multipartita , lo que permite que múltiples 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.

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 tictac de un reloj abstracto. Al igual que en CCS, TPL presenta un prefijo de acción y se puede describir como paciente , es decir, un proceso.${\displaystyle aP}$aceptará ociosamente el tictac del reloj, escrito como

${\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 funcionara, otro para comportarse como si no pudiera, es decir

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

siempre que el proceso E no impida que el reloj siga funcionando.

${\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 maneras de evitar que el reloj siga corriendo. La primera es mediante la presencia del operador ω, por ejemplo en el proceso.${\displaystyle a.P+\Omega }$Se impide que el reloj siga funcionando. Se puede decir que la acción a es insistente , es decir, insiste en actuar antes de que el reloj pueda volver a funcionar.

La segunda forma de evitar el tictac es mediante el 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. Así, si dos procesos paralelos pueden sincronizarse en un instante dado, el reloj no puede funcionar.

Así pues, una forma sencilla de ver la sincronización entre múltiples partes es que un grupo de procesos compuestos permitirá que transcurra el tiempo siempre que ninguno de ellos lo impida, es decir, que el sistema esté de acuerdo en que es hora de seguir adelante.

• Matthew Hennessy y Tim Regan  : Un álgebra de procesos para sistemas temporizados . Information and Computation, 1995.