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

Algebra of communicating processes

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

Неформальное описание

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

Примитивы

ACP использует мгновенное, атомные действия () как его примитивы. Некоторые действия имеют особое значение, например, действие , который представляет тупик или застой, и действие , который представляет собой тихое действие (абстрактные действия, не имеющие конкретной идентичности).

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

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

  • Выбор и последовательность - наиболее фундаментальными алгебраическими операторами являются альтернатива оператор (), который предоставляет выбор между действиями, и оператор последовательности (), который определяет порядок действий. Так, например, процесс
сначала выбирает выполнить либо или же , а затем выполняет действие . Как выбор между и сделано не имеет значения и оставлено неопределенным. Обратите внимание, что альтернативная композиция коммутативна, а последовательная композиция - нет (потому что время течет вперед).
  • Параллелизм - чтобы позволить описание параллелизма, ACP предоставляет слияние и левое слияние операторы. Оператор слияния, , представляет собой параллельную композицию двух процессов, отдельные действия которых чередуются. Оператор слияния слева, , является вспомогательным оператором с семантикой, аналогичной слиянию, но обязательством всегда выбирать свой начальный шаг из левого процесса. Например, процесс
может выполнять действия в любой из последовательностей . С другой стороны, процесс
может выполнять только последовательности поскольку операторы слияния слева гарантируют, что действие происходит первым.
  • Коммуникация - взаимодействие (или коммуникация) между процессами представляется с помощью оператора двоичной связи, . Например, действия и может быть интерпретировано как чтение и запись элемента данных , соответственно. Тогда процесс
сообщит ценность от правого компонентного процесса к левому компонентному процессу (т.е. идентификатор привязан к значению , и бесплатные экземпляры в процессе принять это значение), а затем вести себя как слияние и .
  • Абстракция - оператор абстракции, , это способ «скрыть» определенные действия и рассматривать их как внутренние события моделируемой системы. Абстрагированные действия преобразуются в тихий шаг действие . В некоторых случаях эти тихие шаги также можно удалить из выражения процесса как часть процесса абстракции. Например,
которое в этом случае сводится к
с момента события больше не наблюдается и не имеет наблюдаемых эффектов.

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

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

Алгебра основных процессов

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

Тупик

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

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

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

Когда оператор связи применяется только к действиям, а не к процессам, он интерпретируется как бинарная функция от действий к действиям, . Определение этой функции определяет возможные взаимодействия между процессами - те пары действий, которые не составляют взаимодействия, отображаются на действие тупика, , в то время как разрешенные пары взаимодействий отображаются на соответствующие одиночные действия, представляющие возникновение взаимодействия. Например, функция связи может указывать, что

что указывает на то, что успешное взаимодействие будет сведено к действию . ACP также включает оператор инкапсуляции, для некоторых , который используется для преобразования неудачных попыток связи (т. е. элементов которые не были уменьшены с помощью функции связи) до действия тупика. Аксиомы, связанные с функцией связи и оператором инкапсуляции, следующие:[3]

Абстракция

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

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

Связанные формализмы

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

Рекомендации

  1. ^ J.C.M. Баэтен, Краткая история алгебры процессов, Отчет CSR 04-02, Vakgroep Informatica, Технический университет Эйндховена, 2004 г.
  2. ^ Бас Луттик, Что такое алгебраика в теории процессов, Вычисления алгебраических процессов: первые двадцать пять лет и далее В архиве 2005-12-04 в Wayback Machine, Бертиноро, Италия, 1 августа 2005 г.
  3. ^ а б c d J.A. Бергстра и Дж. Клоп, ACPτ: Универсальная система аксиом для спецификации процессов, CWI Quarterly 15, стр. 3-23, 1987 г.
  4. ^ P.J.L. Кейперс и М.А.Ренирс, Алгебра гибридных процессов, Технический отчет, Департамент математики и информатики, Технический университет Эйндховена, 2003 г.