통신 프로세스의 대수

커뮤니케이션 프로세스의 대수(ACP)는 동시 시스템에 대한 추론에 대한 대수적 접근법이다.이것은 프로세스 대수학 또는 프로세스 계산으로 알려진 수학 동시성 이론의 일원입니다.ACP는 1982년 ^[1]Jan Bergstra와 Jan Willem Klop에 의해 보호되지 않은 재귀 방정식의 해답을 조사하기 위한 노력의 일환으로 처음 개발되었다.다른 주요 프로세스 계산(CCS 및 CSP)보다 ACP의 개발은 프로세스의 대수에 초점을 맞추고 프로세스에 ^[2]대한 추상적이고 일반적인 공리 시스템을 구축하려고 했습니다.실제로 프로세스 대수는 ^{[citation needed]}ACP로 이어진 연구 중에 만들어졌습니다.

비공식적인 설명

ACP는 기본적으로 보편대수의 의미에서의 대수이다.이 대수는 다른 프로세스 또는 특정 원시 요소의 구성을 정의하는 대수적 프로세스 표현식의 관점에서 시스템을 설명하는 방법입니다.

원어민

ACP는 순간적인 원자 ${\displaystyle \mathit{}\mathit{(}\mathit{a}\mathit{,}}$ ${\displaystyle \mathit{b}\mathit{,}}$ c${\displaystyle \mathit{,}}$ $...,$ \$displaystyle {a, b, c,$ ...)을 사용합니다.$\}\}\})$를 원점으로 합니다$.$교착 상태 $또는{\displaystyle }$ 정체 상태를 나타내는 액션 $"\displaystyle\delta$ 및 사일런트액션(특정 식별 정보가 없는 추출된 액션)을 나타내는 액션 $"\displaystyle\tau$와 같은 특별한 의미가 있는 액션도 있습니다.

대수 연산자

작업을 결합하여 다양한 연산자를 사용하여 프로세스를 구성할 수 있습니다.이러한 연산자는 대략 기본 프로세스 대수, 동시성 및 통신을 제공하는 것으로 분류할 수 있습니다.

• 선택과 시퀀스– 대수 연산자의 가장 기본적인 것은 액션의 선택을 제공하는 대체 연산자$(+\displaystyle +)$와 액션의 순서를 지정하는 시퀀스 연산자( ${\\displaystyle\cdot)$입니다.예를 들어, 이 프로세스는

$\displaystyle (a+b)\cdot c}$

에서는 먼저$$\$displaystyle\mathit {a}$ $또는$ b$\$중 $하나$를 실행하고 $다음$으로 동작 c$\$를 수행합니다.\$displaystyle\mathit {a}$과 b$\$의 선택은 중요하지 않으며 발음되지 않습니다.대체 구성은 가환성이지만 순차 구성은 그렇지 않다(시간이 앞으로 흐르기 때문에).

• 동시성: 동시성을 기술할 수 있도록 ACP는 Marge 연산자와 Left-Merge 연산자를 제공합니다.병합 연산자 \$displaystyle \vert$ \$vert$는 개별 작업이 인터리브되는 두 프로세스의 병렬 구성을 나타냅니다.왼쪽 머지 연산자 $"\displaystyle \vert \lfloor$는 Marge와 시멘틱스가 비슷하지만 항상 왼쪽 프로세스에서 첫 번째 단계를 선택하도록 하는 보조 연산자입니다.예를 들어, 프로세스는

$\displaystyle (a\cdot b)\vert \vert (c\cdot d)}$

는 ${\displaystyle a}$${\displaystyle ,}$ ${\displaystyle b}$${\displaystyle ,}$ ${\displaystyle c,}$ ${\displaystyle d}$$\displaystyle$ a$,$${\displaystyle b,}$$$${\displaystyle c}$ ${\displaystyle d,}$ ${\displaystyle c}$ ${\displaystyle d,}$ c ${\displaystyle d}$, ${\displaystyle c}$ d, c ${\displaystyle d,}$ c d, c d ${\displaystyle b}$, c d$,$ c ${\displaystyle d}$, c $db$, $cdb, cdb,$ cdb, cdb, $cdb$ cdb 등의$$ ${\displaystyle \mathrm{순서}}$로 $액션$을 실행할 수 있습니다.그 이외의 경우 프로세스는 다음과 같습니다.

$\displaystyle (a\cdot b)\vert \lfloor (c\cdot d)}$

는 ${\displaystyle b}$ ${\displaystyle c}$$$${\displaystyle d,}$ ${\displaystyle c}$ b ${\displaystyle d,}$ c ${\displaystyle d}$ ${\displaystyle b}$ d, $c$ ${\displaystyle d}$ b b$${ $db$$$} 의 $시퀀스$만 실행할 수 있습니다.좌측 연산자가 먼저$액션$을 $실행하도록 하기$ 때문입니다.

• 통신 — 프로세스 간의 상호 작용(또는 통신)은 이진 통신 연산자${\displaystyle }${\$displaystyle \vert$을(를) 사용하여 나타냅니다. 예를 들어${\displaystyle ,}$ $r{\displaystyle }$ (${\displaystyle d}$) { $displaystyle$r ($d)}$${\displaystyle }$$및{\displaystyle }$w ( ${\displaystyle d}$) { ${\displaystyle \mathrm{displaystyle}}$$$w ($d)}$는 데이터 $항목$의 읽기 및 ${\displaystyle \mathrm{쓰기}}$로${\displaystyle \mathrm{해석}}$될${\displaystyle }$수 있습니다${\displaystyle .}$$}$ ${{displaystyle d\$in$$D$=\{1,2$,3$,\$ldots${\displaystyle \backslash \}\}.}$그 후 프로세스

$\displaystyle \left(\sum _{d\in D}r(d)\cdot y\right)\vert(w(1)\cdot z)}$

는 오른쪽 컴포넌트 프로세스에서 왼쪽 컴포넌트 프로세스($식별자{\displaystyle \mathrm{}}$$$d\$displaystyle$ {$d})$로 값$$1$(\displaystyle$${$d$\})$을 전달하고 $프로세스$에서 d$\$$displaystyle {$$d}$의 $자유{\displaystyle \mathit{}}$ 인스턴스 d$\$displaystyle {$d$})를 전달합니다$$.$${$y}}$은(는) 이 값을 가져와서 y$\displaystyle\mathit$$${y}와 z$\displaystyle\$mathit {$z}$의$$결합으로 동작합니다$.$

• 추상화 - 추상화 연산자 ${\displaystyle i_{}}$I \ $displaystyle$\$tau$_ {$I$는 특정 액션을 "숨김"하여 모델링되는 시스템 내부의 이벤트로 취급하는 방법입니다.추상화된 액션은 사일런트스텝 $액션$으로 변환됩니다$.(\displaystyle\tau$ 이러한 사일런트스텝은 추상화 프로세스의 일부로서 프로세스 표현에서 삭제될 수도 있습니다.예를들면,

$\displaystyle \{c\}}((a+b)\cdot c)=(a+b)\cdot \cdot }$

이 경우, 이 경우, 이 값은

${\displaystyle a+b}$

이벤트 $(\$ {c$})$는 더 이상 관찰할 수 없고 관찰할 수 있는 효과가 없기 때문입니다.

형식적 정의

ACP는 기본적으로 다양한 연산자의 공식 정의에 대해 자명한 대수적 접근방식을 채택한다.아래에 제시된 공리는 ACP(추상화가 있는 ACP)에_{${\displaystyle \tau }$} 대한 완전한 공리 시스템을 구성합니다.

기본 프로세스 대수

대체 및 순차 합성 연산자를 사용하여 ACP는 공리를^[3] 만족시키는 기본 프로세스 대수를 정의합니다.

$(\displaystyle\displaystyle\x+y&=(x+y)+z&=(x+y)\cdot z&=(x+y)\cdot z&=(y\cdot z)\(x\cdot y)\cdot z&cdot z=(x\cdot y)\cdot z&x\cdot z&x\cdot;\cdot\cdot;\cdot;\cdot z&y\cdot$

교착 상태

기본 대수 이외에, 두 개의 추가 공리가 대체 연산자와 시퀀스 연산자 및 교착 작용 $사이$의 관계를 정의합니다. $§$ ${\displaystyle$ \$delta$}

$(\displaystyle\displaystyle+x&=&x\displaystyle\displaystyle\displays +x&=&x\cdot x&\cdot\end{display})$

동시성과 상호작용

Marge 연산자, Left-Merge 연산자 및 통신 연산자와^[3] 관련된 공리는 다음과 같습니다.

${\displaystyle{\begin{행렬}x\vert \vert y&, =&,x\vert\lfloory+y\vert\lfloor x+x\vert y\\a\cdotx\vert \lfloor y&, =&, a\cdot(x\vert\vert y)\\a\vert \lfloor y&, =&, a\cdot y\\(x+y)\vert \lfloor z&, =&,(\lfloor zx\vert)+(\lfloor zy\vert)\\a\cdotx\vert b&, =&,(a\vert b)\cdotx\\a\vert b\cdot x&, =&,(a\vert b)\cdo.T, =&,(a\vert b)\cdot(x.x\vert b\cdot y& x\\a\cdot\vert \vert y)\(x+y)\vert z&=&x\vert z+y\vert z\x\vert (y+z)&=&x\vert y+x\vert z\end{vert}}$

통신 사업자가 프로세스가 아닌 조치에만 적용되는 경우, ${\displaystyle A}$× ${\displaystyle A}$ ${\displaystyle A}$ \$displaystyle \vert$$A\times$ A$\rightarrow$ A$.$ 이 함수의 정의는 프로세스 간에 가능한 상호작용을 정의합니다. 상호작용을 구성하지 않는 액션의 쌍은 교착 $액션$인 \$displaystyle \delta$에 매핑되며 허용된 상호작용 쌍은 다음과 같은 단일 액션에 매핑됩니다.상호 작용예를 들어, 통신 함수는 다음과 같이 지정할 수 있습니다.

$오른쪽 화살표 c를 표시합니다.$

$ACP에는$$$$실패$한 통신 $시도$를 변환하기 위해 사용되는 일부$H$의 ${\displaystyle \mathrm{캡슐화}}$ 연산자 ${\displaystyle H_{}}$$displaystyle\partial_$${H$$\})$도 포함되어 있습니다.즉, 통신 기능을 통해 감소되지 않은$$H($디스플레이 스타일$ H$)$ $요소$를 교착 상태로 만듭니다.통신 함수 및 캡슐화 연산자와^[3] 관련된 공리는 다음과 같습니다.

${\displaystyle{\begin{행렬}a\vert b&, =&,b\vert a\\(a\vert b)\vert c&, =&,a\vert(b\vert c)\\a\vert \delta&=&,\delta\\\partial _ᆱ(를)&, =&, a{\mbox{만약}}a\notin H\\\partial _ᆳ(를)&, =&, \delta{\mbox{만약}}a\in H\\\partial _ᆵ(x+y)&, =&,\partial _ᆶ())+\partial _ᆷ(y)\\\partial _ᆸ(이x\cdot)&, =&, \part.ial _ᆪ())\cdot\partial _ᆫ(y)\\\end{매트릭스}}}$

추상화

추상화 연산자와^[3] 관련된 공리는 다음과 같습니다.

${\displaystyle{\begin{행렬}\tau _ᆳ(\tau)&, =&,\tau \\\tau _ᆴ(를)&, =&, a{\mbox{만약}}a\notin I\\\tau _ᆶ(를)&, =&, \tau{\mbox{만약}}a\in I\\\tau _ᆸ(x+y)&, =&, \tau _ᆹ())+\tau _ᆺ(y)\\\tau _ᆻ(이x\cdot)&, =&, \tau _ᆼ())\cdot\tau _ᆽ(y)\\\partial _ᆾ(\tau)&, =&, \tau\\x\cdot \tau&=&,x\\\tau \cdot. X&, =&, \tau\cdot x+x\\a\cdot(\tau \cdot x+y)&, =&, a\cdot(\t.au \cdot x + y ) + a\cdot x\\cdot x\vert \lfloor y=&\cdot \cdot \cdot (x\vert \vert y)\\cdot \lfloor x=&\cdot x=\cdot x=\cdot;\cdot x&\cdot;\cdot;\cdot;\cdot \cdot;\cdot x\vert \cdot;\cdot x\vert \cdot;\cdot$

상기 목록의 액션a는 값 "을 가질 수 있습니다(물론 "는 추상화 세트I에 속할 수 없습니다).

관련 형식

ACP는 다음과 같은 동시 시스템을 기술 및 분석하는 데 사용할 수 있는 다른 몇 가지 형식주의의 기초 또는 영감이 되어 왔습니다.

• PSF
• μCRL
• mCRL2
• HyPA - 하이브리드^[4] 시스템용 프로세스 대수

레퍼런스