Алгебра коммуникативных процессов

Алгебра взаимодействующих процессов (АКТ) представляет собой алгебраический подход к рассуждению о параллельных системах . Это член семейства математических теорий параллелизма, известных как алгебры процессов или исчисления процессов . ACP был первоначально разработан Яном Бергстра и Яном Виллемом Клопом в 1982 году ^[1] как часть усилий по исследованию решений неохраняемых рекурсивных уравнений. В большей степени, чем другие основополагающие исчисления процессов ( CCS и CSP ), разработка ACP была сосредоточена на алгебре процессов и была направлена ​​на создание абстрактной обобщенной аксиоматической системы для процессов ^[2].и фактически термин « алгебра процессов» был введен в обращение во время исследования, которое привело к ACP.

Неофициальное описание [ править ]

ACP - это, по сути, алгебра в смысле универсальной алгебры . Эта алгебра представляет собой способ описания систем в терминах выражений алгебраических процессов, которые определяют композиции других процессов или определенных примитивных элементов.

Примитивы [ править ]

ACP в качестве примитивов использует мгновенные атомарные действия ( ). Некоторые действия имеют особое значение, например действие , которое представляет тупик или застой, и действие , которое представляет собой молчаливое действие (абстрактные действия, не имеющие определенного идентификатора).${\ displaystyle {\ mathit {a, b, c, ...}}}$${\ displaystyle \ delta}$${\ Displaystyle \ тау}$

Алгебраические операторы [ править ]

Действия можно комбинировать для формирования процессов с помощью множества операторов. Эти операторы можно условно разделить на категории, обеспечивающие базовую алгебру процессов , параллелизм и обмен данными .

• Выбор и последовательность - наиболее фундаментальными из алгебраических операторов являются альтернативный оператор ( ), который обеспечивает выбор между действиями, и оператор последовательности ( ), который определяет порядок действий. Так, например, процесс${\ displaystyle +}$${\ displaystyle \ cdot}$

${\ displaystyle (а + b) \ cdot c}$

сначала выбирает выполнение либо или , а затем выполняет действие . Как делается выбор между и, не имеет значения и остается неопределенным. Обратите внимание, что альтернативная композиция коммутативна, а последовательная композиция - нет (потому что время течет вперед).${\ Displaystyle {\ mathit {а}}}$${\ displaystyle {\ mathit {b}}}$${\ displaystyle {\ mathit {c}}}$${\ Displaystyle {\ mathit {а}}}$${\ displaystyle {\ mathit {b}}}$

• Параллелизм - чтобы позволить описание параллелизма, ACP предоставляет операторы слияния и слияния слева . Оператор слияния , представляет собой параллельную композицию двух процессов, отдельные действия которых чередуются. Левый оператор слияния,, является вспомогательным оператором с семантикой, аналогичной слиянию, но обязательством всегда выбирать свой начальный шаг из левого процесса. Например, процесс${\ Displaystyle \ верт \ верт}$${\ displaystyle \ vert \ lfloor}$

${\ Displaystyle (а \ cdot b) \ верт \ верт (с \ cdot d)}$

может выполнять действия в любой из последовательностей . С другой стороны, процесс${\ displaystyle a, b, c, d}$${\ displaystyle abcd, acbd, acdb, cabd, cadb, cdab}$

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

может выполнять только последовательности, поскольку операторы слияния слева гарантируют, что действие произойдет первым.${\displaystyle abcd,acbd,acdb}$${\displaystyle {\mathit {a}}}$

• Связь - взаимодействие (или связь) между процессами представлена с использованием оператора двоичной связи, . Например, действия и могут быть интерпретированы как чтение и запись элемента данных соответственно. Тогда процесс${\displaystyle \vert }$${\displaystyle r(d)}$${\displaystyle w(d)}$${\displaystyle d\in D=\{1,2,3,\ldots \}}$

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

будет передавать значение из правого компонентного процесса в левый компонентный процесс ( т. е. идентификатор привязан к значению , а свободные экземпляры в процессе принимают это значение), а затем ведут себя как слияние и .${\displaystyle 1}$${\displaystyle {\mathit {d}}}$${\displaystyle 1}$${\displaystyle {\mathit {d}}}$${\displaystyle {\mathit {y}}}$${\displaystyle {\mathit {y}}}$${\displaystyle {\mathit {z}}}$

• Абстракция - оператор абстракции, это способ «скрыть» определенные действия и рассматривать их как события, которые являются внутренними для моделируемых систем. Абстрагированные действия преобразуются в бесшумное пошаговое действие . В некоторых случаях эти тихие шаги также могут быть удалены из выражения процесса как часть процесса абстракции. Например,${\displaystyle \tau _{I}}$${\displaystyle \tau }$

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

которое в этом случае можно свести к

${\displaystyle a+b}$

поскольку событие больше не является наблюдаемым и не имеет наблюдаемых эффектов.${\displaystyle {\mathit {c}}}$

Формальное определение [ править ]

ACP принципиально использует аксиоматический алгебраический подход к формальному определению своих различных операторов. Представленные ниже аксиомы составляют полную аксиоматическую систему для ACP (ACP с абстракцией)._{${\displaystyle \tau }$}

Алгебра основных процессов [ править ]

Используя альтернативные и последовательные операторы композиции, ACP определяет базовую алгебру процессов, удовлетворяющую аксиомам ^[3]

${\displaystyle {\begin{matrix}x+y&=&y+x\\(x+y)+z&=&x+(y+z)\\x+x&=&x\\(x+y)\cdot z&=&(x\cdot z)+(y\cdot z)\\(x\cdot y)\cdot z&=&x\cdot (y\cdot z)\end{matrix}}}$

Тупик [ править ]

Помимо базовой алгебры, две дополнительные аксиомы определяют отношения между альтернативными операторами и операторами последовательности, а также действием тупика ,${\displaystyle \delta }$

${\displaystyle {\begin{matrix}\delta +x&=&x\\\delta \cdot x&=&\delta \end{matrix}}}$

Параллелизм и взаимодействие [ править ]

Аксиомы, связанные с операторами слияния, слияния слева и связи, следующие: ^[3]

${\displaystyle {\begin{matrix}x\vert \vert y&=&x\vert \lfloor y+y\vert \lfloor x+x\vert y\\a\cdot x\vert \lfloor y&=&a\cdot (x\vert \vert y)\\a\vert \lfloor y&=&a\cdot y\\(x+y)\vert \lfloor z&=&(x\vert \lfloor z)+(y\vert \lfloor z)\\a\cdot x\vert b&=&(a\vert b)\cdot x\\a\vert b\cdot x&=&(a\vert b)\cdot x\\a\cdot x\vert b\cdot y&=&(a\vert b)\cdot (x\vert \vert y)\\(x+y)\vert z&=&x\vert z+y\vert z\\x\vert (y+z)&=&x\vert y+x\vert z\end{matrix}}}$

Когда оператор связи применяются к действиям в одиночку, а не процессам, он интерпретируется как двоичные функции от действий к действиям, . Определение этой функции определяет возможные взаимодействия между процессами - те пары действий, которые не составляют взаимодействия, отображаются на действие тупика , а разрешенные пары взаимодействий отображаются на соответствующие одиночные действия, представляющие возникновение взаимодействия. Например, функция связи может указывать, что${\displaystyle \vert :A\times A\rightarrow A}$${\displaystyle \delta }$

${\displaystyle a\vert a\rightarrow c}$

что указывает на то, что успешное взаимодействие сведется к действию . ACP также включает в себя оператор инкапсуляции для некоторых , который используется для преобразования неудачных попыток связи (т. Е. Элементы , которые не были сокращены с помощью функции связи) в действие тупика. Аксиомы, связанные с функцией связи и оператором инкапсуляции, следующие: ^[3]${\displaystyle a\vert a}$${\displaystyle c}$${\displaystyle \partial _{H}}$${\displaystyle H\subseteq A}$${\displaystyle H}$

${\displaystyle {\begin{matrix}a\vert b&=&b\vert a\\(a\vert b)\vert c&=&a\vert (b\vert c)\\a\vert \delta &=&\delta \\\partial _{H}(a)&=&a{\mbox{ if }}a\notin H\\\partial _{H}(a)&=&\delta {\mbox{ if }}a\in H\\\partial _{H}(x+y)&=&\partial _{H}(x)+\partial _{H}(y)\\\partial _{H}(x\cdot y)&=&\partial _{H}(x)\cdot \partial _{H}(y)\\\end{matrix}}}$

Абстракция [ править ]

Аксиомы, связанные с оператором абстракции, следующие: ^[3]

${\displaystyle {\begin{matrix}\tau _{I}(\tau )&=&\tau \\\tau _{I}(a)&=&a{\mbox{ if }}a\notin I\\\tau _{I}(a)&=&\tau {\mbox{ if }}a\in I\\\tau _{I}(x+y)&=&\tau _{I}(x)+\tau _{I}(y)\\\tau _{I}(x\cdot y)&=&\tau _{I}(x)\cdot \tau _{I}(y)\\\partial _{H}(\tau )&=&\tau \\x\cdot \tau &=&x\\\tau \cdot x&=&\tau \cdot x+x\\a\cdot (\tau \cdot x+y)&=&a\cdot (\tau \cdot x+y)+a\cdot x\\\tau \cdot x\vert \lfloor y&=&\tau \cdot (x\vert \vert y)\\\tau \vert \lfloor x&=&\tau \cdot x\\\tau \vert x&=&\delta \\x\vert \tau &=&\delta \\\tau \cdot x\vert y&=&x\vert y\\x\vert \tau \cdot y&=&x\vert y\end{matrix}}}$

Обратите внимание, что действие a в приведенном выше списке может принимать значение δ (но, конечно, δ не может принадлежать множеству абстракций I ).

Связанные формализмы [ править ]

ACP послужил основой или вдохновением для нескольких других формализмов, которые можно использовать для описания и анализа параллельных систем, включая:

• PSF
• μCRL
• mCRL2
• HyPA - алгебра процессов для гибридных систем ^[4]

Ссылки [ править ]