임시 프로세스 언어

이론 컴퓨터 과학에서, TPL(Temporal Process Language)은 다중 파티 동기화 개념으로 로빈 밀너의 CCS를 확장하는 프로세스 미적분입니다. 다중 프로세스는 글로벌 '클럭' 상에서 동기화할 수 있습니다.이 클럭은 시간을 측정합니다.구체적으로는 아니지만 전체 프로세스가 언제 진행될 수 있는지를 정의하는 추상적인 신호입니다.

비공식 정의

TPL은 CCS의 보수적인 확장으로, 프로세스에 의한 시간의 흐름을 나타내는 ▲라는 특별한 액션이 추가되어 추상적인 클럭의 똑딱거림입니다.CCS와 마찬가지로 TPL은 액션프리픽스를 특징으로 하며 참을성 있는 것으로 설명할 수 있습니다.${\displaystyle 즉}$, $프로세스{\displaystyle }$ a${\displaystyle .}$ P$.\displaystyle$ a$.$$P}$은(는) 다음과 같이 쓰여진 시계의 똑딱거림을 받습니다.

$(\displaystyle a).오른쪽 화살표 ^{a}a.P}$

추상시간 사용의 열쇠는 타임아웃 연산자로, 2개의 프로세스를 제시합니다.하나는 클럭이 틱인 것처럼 동작하고, 다른 하나는 할 수 없는 것처럼 동작합니다.

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

단, 프로세스E는 클럭의 똑딱거림을 방해하지 않습니다.

$\displaystyle \lfloor (F)\right 화살표 ^{\sigma }E'}$

단, E가 E'가 되기 위한 액션a를 실행할 수 있는 경우.

TPL에서는 클럭이 똑딱거리지 않도록 하는 방법이 두 가지 있습니다.첫 번째는 예를 들어 .${\displaystyle P}$+$$ \ $displaystyle$a${\displaystyle }$등의 조작자의 존재에 의한 것입니다.$P$$+\Omega }$ 클럭이 똑딱거리지 않습니다.동작 a는 집요하다고 할 수 있습니다.즉, 클럭이 다시 똑딱거리기 전에 동작해야 한다고 주장합니다.

똑딱거리는 것을 막을 수 있는 두 번째 방법은 무언의 행동(즉, 행동)이 항상 ①의 행동보다 우선하고, 따라서 ②의 행동을 억제한다는 최대 진보의 개념을 통해서이다.즉, 2개의 병렬 프로세스를 동시에 동기화할 수 있기 때문에 클럭은 틱할 수 없습니다.

따라서, 멀티 파티의 동기화를 간단하게 볼 수 있는 방법은, 구성된 프로세스 그룹이, 어느 프로세스도 그것을 막지 않는 한, 즉, 시스템이 이행할 시점이라고 하는 것에 동의하는 경우, 시간이 경과할 수 있도록 하는 것입니다.

형식적 정의

구문

a는 비사일런트액션명, α는 임의의 액션명(사일런트액션 포함), X는 재귀에 사용되는 프로세스라벨로 하겠습니다

${\displaystyle\begin{matrix}프로세스:= &\alpha 입니다.Proc\ 및 lfloor Proc\rfloor(Proc)\ 및 Proc+Proc\; Proc\\recX.Proc\ & X\ & Omega\ & Proc\ setminus a\ & 0\ \ end { matrix }$

레퍼런스

Matthew Hennessy and Tim Regan : Timed Systems의 프로세스 대수.정보와 계산, 1995.