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

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

Неофициальное описание

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

Примитивы

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

Алгебраические операторы

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

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

(a+b)\cdot c

сначала решает выполнить либо

{\mathit {a}}

или

{\mathit {b}}

, а затем выполняет действие

{\mathit {c}}

. Как происходит выбор между

{\mathit {a}}

и

{\mathit {b}}

сделано, не имеет значения и остается неопределенным. Обратите внимание, что альтернативная композиция коммутативна, а последовательная композиция — нет (поскольку время течет вперед).

Параллелизм — чтобы обеспечить описание параллелизма, ACP предоставляет операторы слияния и левого слияния . Оператор слияния, $\vert \vert$ , представляет собой параллельную композицию двух процессов, отдельные действия которых чередуются. Оператор левого слияния, $\vert \lfloor$ , — это вспомогательный оператор с семантикой, аналогичной слиянию, но с обязательством всегда выбирать начальный шаг из левого процесса. В качестве примера процесс

(a\cdot b)\vert \vert (c\cdot d)

может выполнять действия

a,b,c,d

в любой из последовательностей

abcd,acbd,acdb,cabd,cadb,cdab

. С другой стороны, процесс

(a\cdot b)\vert \lfloor (c\cdot d)

может выполнять только последовательности

abcd,acbd,acdb

поскольку операторы левого слияния гарантируют, что действие

{\mathit {a}}

происходит первым.

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

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

сообщит ценность

1

от процесса правого компонента к процессу левого компонента ( т.е. идентификатор

{\mathit {d}}

привязан к значению

1

и бесплатные экземпляры

{\mathit {d}}

в процессе

{\mathit {y}}

принять это значение), а затем вести себя как слияние

{\mathit {y}}

и

{\mathit {z}}

.

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

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

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

a+b

с момента события

{\mathit {c}}

больше не наблюдаемо и не имеет наблюдаемых эффектов.

Формальное определение

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

Базовая алгебра процессов

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

{\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}}

Тупик

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

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

Параллелизм и взаимодействие

Аксиомы, связанные с операторами слияния, левого слияния и связи: ^{[ 3 ]}

{\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}}

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

a\vert a\rightarrow c

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

{\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 ]}

{\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 послужил основой или источником вдохновения для нескольких других формализмов, которые можно использовать для описания и анализа параллельных систем, в том числе:

ПСФ
µCRL
mCRL2
HyPA — алгебра процессов для гибридных систем ^{[ 4 ]}

Ссылки

^ JCM Baeten, Краткая история алгебры процессов , Отчет CSR 04-02, факультет компьютерных наук, Технологический университет Эйндховена, 2004 г.
^ Бас Люттик, Что такое алгебраика в теории процессов , Исчисления алгебраических процессов: первые двадцать пять лет и позже. Архивировано 4 декабря 2005 г. в Wayback Machine , Бертиноро, Италия, 1 августа 2005 г.
^ Jump up to: ^а ^б ^с ^д Дж. А. Бергстра и Дж. В. Клоп, ACP _τ : Универсальная система аксиом для спецификации процессов , CWI Quarterly 15, стр. 3–23, 1987 г.
^ П. Дж. Л. Куйперс и М. А. Ренье, Алгебра гибридных процессов , Технический отчет, факультет математики и информатики, Технический университет Эйндховена, 2003 г.

[baeten2004-1] JCM Baeten, Краткая история алгебры процессов , Отчет CSR 04-02, факультет компьютерных наук, Технологический университет Эйндховена, 2004 г.

[luttik2005-2] Бас Люттик, Что такое алгебраика в теории процессов , Исчисления алгебраических процессов: первые двадцать пять лет и позже. Архивировано 4 декабря 2005 г. в Wayback Machine , Бертиноро, Италия, 1 августа 2005 г.

[bergstraklop1987-3] Jump up to: ^а ^б ^с ^д Дж. А. Бергстра и Дж. В. Клоп, ACP _τ : Универсальная система аксиом для спецификации процессов , CWI Quarterly 15, стр. 3–23, 1987 г.

[CuijpersReiners2003-4] П. Дж. Л. Куйперс и М. А. Ренье, Алгебра гибридных процессов , Технический отчет, факультет математики и информатики, Технический университет Эйндховена, 2003 г.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

v т и Параллельные вычисления
Общий	Параллелизм Управление параллелизмом Параллельные структуры данных Параллельные хэш-таблицы Одновременные пользователи Неопределенность Линеаризуемость
Процесс исчисления	CSP CCS АШП ЛОТОС π-исчисление Окружающее исчисление API-исчисление БУМАГА Джойн-исчисление
Классические задачи	проблема ABA Проблема курильщиков сигарет Тупик Проблема обедающих философов Проблема производителя и потребителя Состояние гонки Проблема читателей и писателей Проблема со спящим парикмахером
Категория: Параллельные вычисления