Процесс исчисления

Семейство подходов для моделирования параллельных систем

В информатике исчисления процессов ( или алгебры процессов ) представляют собой разнообразное семейство связанных подходов для формального моделирования параллельных систем . Исчисления процессов предоставляют инструмент для высокоуровневого описания взаимодействий, коммуникаций и синхронизаций между набором независимых агентов или процессов. Они также предоставляют алгебраические законы, которые позволяют манипулировать описаниями процессов и анализировать их, а также допускают формальные рассуждения об эквивалентностях между процессами (например, с использованием бисимуляции ). Ведущие примеры исчислений процессов включают CSP , CCS , ACP и LOTOS . ^[1] Более поздние дополнения к семейству включают π-исчисление , окружающее исчисление , PEPA , исчисление слияния и исчисление соединения .

Основные характеристики

Хотя разнообразие существующих исчислений процессов очень велико (включая варианты, включающие стохастическое поведение, временную информацию и специализации для изучения молекулярных взаимодействий), есть несколько общих черт, присущих всем исчислениям процессов: ^[2]

• Представление взаимодействия между независимыми процессами как коммуникации ( передачи сообщений ), а не как изменения общих переменных.
• Описание процессов и систем с использованием небольшого набора примитивов, а также операторов для объединения этих примитивов.
• Определение алгебраических законов для операторов процесса, которые позволяют манипулировать выражениями процесса с использованием эквациональных рассуждений .

Математика процессов

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

• параллельная композиция процессов
• указание того, какие каналы использовать для отправки и получения данных
• последовательность взаимодействий
• скрытие точек взаимодействия
• рекурсия или репликация процесса

Параллельная композиция

Параллельная композиция двух процессов и , обычно записываемая как , является ключевым примитивом, отличающим исчисления процессов от последовательных моделей вычислений. Параллельная композиция позволяет вычислениям в и происходить одновременно и независимо. Но она также допускает взаимодействие, то есть синхронизацию и поток информации от к (или наоборот) по каналу, общему для обоих. Важно то, что агент или процесс может быть подключен к нескольким каналам одновременно. ${\displaystyle {\mathit {P}}}$ ${\displaystyle {\mathit {Q}}}$ ${\displaystyle P\vert Q}$ ${\displaystyle {\mathit {P}}}$ ${\displaystyle {\mathit {Q}}}$ ${\displaystyle {\mathit {P}}}$ ${\displaystyle {\mathit {Q}}}$

Каналы могут быть синхронными или асинхронными. В случае синхронного канала агент, отправляющий сообщение, ждет, пока другой агент получит сообщение. Асинхронные каналы не требуют такой синхронизации. В некоторых исчислениях процессов (в частности, в π-исчислении ) сами каналы могут отправляться в сообщениях через (другие) каналы, позволяя топологии взаимосвязей процессов изменяться. Некоторые исчисления процессов также позволяют создавать каналы во время выполнения вычисления.

Коммуникация

Взаимодействие может быть (но не всегда) направленным потоком информации. То есть вход и выход можно различать как примитивы двойного взаимодействия. Исчисления процессов, которые делают такие различия, обычно определяют оператор ввода ( например ) и оператор вывода ( например ), оба из которых называют точку взаимодействия (здесь ), которая используется для синхронизации с примитивом двойного взаимодействия. ${\displaystyle x(v)}$ ${\displaystyle x\langle y\rangle }$ ${\displaystyle {\mathit {x}}}$

Если информация будет обмениваться, она будет перетекать из процесса вывода во процесс ввода. Примитив вывода будет определять данные для отправки. В , эти данные — . Аналогично, если вход ожидает получения данных, одна или несколько связанных переменных будут выступать в качестве заполнителей, которые будут заменены данными, когда они поступят. В , играет эту роль. Выбор вида данных, которыми можно обмениваться во взаимодействии, является одной из ключевых особенностей, отличающих различные исчисления процессов. ${\displaystyle x\langle y\rangle }$ ${\displaystyle y}$ ${\displaystyle x(v)}$ ${\displaystyle v}$

Последовательная композиция

Иногда взаимодействия должны быть упорядочены по времени. Например, может быть желательно указать такие алгоритмы, как: сначала получить некоторые данные на , а затем отправить эти данные на ${\displaystyle {\mathit {x}}}$ ${\displaystyle {\mathit {y}}}$ . Последовательная композиция может использоваться для таких целей. Это хорошо известно из других моделей вычислений. В исчислениях процессов оператор секвенирования обычно интегрируется с вводом или выводом, или с обоими. Например, процесс будет ожидать ввода на . Только когда этот ввод произойдет, процесс будет активирован, а полученные данные через заменят идентификатор . ${\displaystyle x(v)\cdot P}$ ${\displaystyle {\mathit {x}}}$ ${\displaystyle {\mathit {P}}}$ ${\displaystyle {\mathit {x}}}$ ${\displaystyle {\mathit {v}}}$

Семантика сокращения

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

${\displaystyle x\langle y\rangle \cdot P\;\vert \;x(v)\cdot Q\longrightarrow P\;\vert \;Q[^{y}\!/\!_{v}]}$

Интерпретация этого правила редукции такова:

1. Процесс отправляет сообщение, здесь , по каналу . Двойственно, процесс получает это сообщение по каналу . ${\displaystyle x\langle y\rangle \cdot P}$ ${\displaystyle {\mathit {y}}}$ ${\displaystyle {\mathit {x}}}$ ${\displaystyle x(v)\cdot Q}$ ${\displaystyle {\mathit {x}}}$
2. После отправки сообщения становится процессом , а становится процессом , в котором заполнитель заменен на , данные, полученные на . ${\displaystyle x\langle y\rangle \cdot P}$ ${\displaystyle {\mathit {P}}}$ ${\displaystyle x(v)\cdot Q}$ ${\displaystyle Q[^{y}\!/\!_{v}]}$ ${\displaystyle {\mathit {Q}}}$ ${\displaystyle {\mathit {v}}}$ ${\displaystyle {\mathit {y}}}$ ${\displaystyle {\mathit {x}}}$

Класс процессов, который допускается в качестве продолжения выходной операции, существенно влияет на свойства исчисления. ${\displaystyle {\mathit {P}}}$

Скрытие

Процессы не ограничивают количество соединений, которые могут быть созданы в данной точке взаимодействия. Но точки взаимодействия допускают интерференцию (т. е. взаимодействие). Для синтеза компактных, минимальных и композиционных систем решающее значение имеет возможность ограничения интерференции. Операции сокрытия позволяют контролировать соединения, созданные между точками взаимодействия при параллельном составлении агентов. Сокрытие может быть обозначено различными способами. Например, в π-исчислении сокрытие имени в может быть выражено как , тогда как в CSP оно может быть записано как . ${\displaystyle {\mathit {x}}}$ ${\displaystyle {\mathit {P}}}$ ${\displaystyle (\nu \;x)P}$ ${\displaystyle P\setminus \{x\}}$

Рекурсия и репликация

Представленные до сих пор операции описывают только конечное взаимодействие и, следовательно, недостаточны для полной вычислимости, которая включает в себя нетерминационное поведение. Рекурсия и репликация — это операции, которые позволяют конечные описания бесконечного поведения. Рекурсия хорошо известна из последовательного мира. Репликация может пониматься как сокращение параллельной композиции счетно бесконечного числа процессов: ${\displaystyle !P}$ ${\displaystyle {\mathit {P}}}$

${\displaystyle !P=P\mid !P}$

Нулевой процесс

Исчисления процессов обычно также включают нулевой процесс (обозначаемый по-разному как , , , , или каким-либо другим подходящим символом), который не имеет точек взаимодействия. Он совершенно неактивен, и его единственное предназначение — действовать как индуктивный якорь, поверх которого могут быть сгенерированы более интересные процессы. ${\displaystyle {\mathit {nil}}}$ ${\displaystyle 0}$ ${\displaystyle {\mathit {STOP}}}$ ${\displaystyle \delta }$

Дискретная и непрерывная алгебра процессов

Алгебра процессов изучалась для дискретного и непрерывного времени (реального времени или плотного времени). ^[4]

История

В первой половине 20-го века были предложены различные формализмы для описания неформальной концепции вычислимой функции , причем μ-рекурсивные функции , машины Тьюринга и лямбда-исчисление, возможно, являются сегодня наиболее известными примерами. Удивительный факт, что они по сути эквивалентны, в том смысле, что все они кодируются друг в друга, подтверждает тезис Чёрча-Тьюринга . Другая общая черта комментируется реже: все они легче всего понимаются как модели последовательных вычислений. Последующая консолидация компьютерной науки потребовала более тонкой формулировки понятия вычисления, в частности явных представлений параллелизма и коммуникации. Модели параллелизма, такие как исчисления процессов, сети Петри в 1962 году и модель актора в 1973 году, возникли из этой линии исследования.

Исследования исчислений процессов начались всерьез с основополагающей работы Робина Милнера по исчислению коммуникабельных систем (CCS) в период с 1973 по 1980 год. « Коммуникационные последовательные процессы » (CSP) К. А. Хоара впервые появились в 1978 году и впоследствии были развиты в полноценное исчисление процессов в начале 1980-х годов. Между CCS и CSP по мере их развития происходило много перекрестного опыления идеями. В 1982 году Ян Бергстра и Ян Виллем Клоп начали работу над тем, что стало известно как Алгебра коммуникабельных процессов (ACP), и ввели термин «алгебра процессов» для описания своей работы. ^[1] CCS, CSP и ACP составляют три основные ветви семейства исчислений процессов: большинство других исчислений процессов могут проследить свои корни до одного из этих трех исчислений.

Текущие исследования

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

• Разработка новых исчислений процессов для лучшего моделирования вычислительных явлений.
• Поиск хорошо ведущих себя подвычислений заданного исчисления процесса. Это ценно, потому что (1) большинство исчислений довольно дикие в том смысле, что они довольно общие и мало что можно сказать о произвольных процессах; и (2) вычислительные приложения редко исчерпывают все исчисление. Скорее, они используют только процессы, которые очень ограничены по форме. Ограничение формы процессов в основном изучается с помощью систем типов .
• Логики для процессов, которые позволяют рассуждать о (по сути) произвольных свойствах процессов, следуя идеям логики Хоара .
• Поведенческая теория: что означает, что два процесса одинаковы? Как мы можем решить, различны ли два процесса или нет? Можем ли мы найти представителей для классов эквивалентности процессов? Обычно процессы считаются одинаковыми, если никакой контекст, то есть другие процессы, работающие параллельно, не могут обнаружить разницу. К сожалению, уточнение этой интуиции является тонким и в основном приводит к громоздким характеристикам равенства (которые в большинстве случаев также должны быть неразрешимыми из-за проблемы остановки ). Бисимуляции — это технический инструмент, который помогает рассуждать об эквивалентностях процессов.
• Выразительность исчислений. Опыт программирования показывает, что некоторые проблемы легче решать на некоторых языках, чем на других. Это явление требует более точной характеристики выразительности исчислений, моделирующих вычисления, чем та, которая предоставляется тезисом Чёрча-Тьюринга . Один из способов сделать это — рассмотреть кодировки между двумя формализмами и посмотреть, какие свойства кодировки могут потенциально сохранить. Чем больше свойств может быть сохранено, тем более выразительной считается цель кодировки. Для исчислений процессов знаменитые результаты заключаются в том, что синхронное π-исчисление более выразительно, чем его асинхронный вариант, имеет ту же выразительную силу, что и π-исчисление более высокого порядка , ^[5], но меньше, чем окружающее исчисление . ^{[ требуется цитата ]}
• Использование исчисления процессов для моделирования биологических систем (стохастическое π-исчисление, BioAmbients, Beta Binders, BioPEPA, исчисление Brane). Некоторые полагают, что композиционность, предлагаемая инструментами теории процессов, может помочь биологам организовать свои знания более формально.

Реализации программного обеспечения

Идеи, лежащие в основе алгебры процессов, привели к появлению нескольких инструментов, в том числе:

• КАПД
• Инструментарий для параллелизма
• набор инструментов mCRL2

Связь с другими моделями параллелизма

Моноид истории — это свободный объект , который в общем случае способен представлять истории отдельных взаимодействующих процессов. Исчисление процессов — это формальный язык, наложенный на моноид истории последовательным образом. ^[6] То есть моноид истории может только записывать последовательность событий с синхронизацией, но не определяет разрешенные переходы состояний. Таким образом, исчисление процессов относится к моноиду истории так же, как формальный язык относится к свободному моноиду (формальный язык — это подмножество множества всех возможных строк конечной длины алфавита, сгенерированного звездой Клини ).

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

Смотрите также

• Коммуникация последовательных процессов
• ProVerif
• Стохастический зонд
• Тамарин Провер
• Язык временных процессов
• π-исчисление

Ссылки

1. Баетен, JCM (2004). «Краткая история алгебры процессов» (PDF) . Раппорт КСО 04-02 . Вакгруппа информатики, Технический университет Эйндховена.
2. Пирс, Бенджамин (1996-12-21). "Основные исчисления для языков программирования". Справочник по компьютерной науке и инжинирингу . CRC Press. С. 2190–2207. ISBN 0-8493-2909-4.
3. Baeten, JCM; Bravetti, M. (август 2005 г.). "A Generic Process Algebra". Algebraic Process Calculi: The First Twenty Five Years and Beyond (BRICS Notes Series NS-05-3) . Bertinoro, Forlì, Italy: BRICS, Department of Computer Science, University of Aarhus . Получено 29.12.2007 .
4. Baeten, JCM; Middelburg, CA (2000). «Алгебра процессов с синхронизацией: реальное время и дискретное время»: 627–684. CiteSeerX 10.1.1.42.729 .  {{cite journal}}: Цитировать журнал требует |journal=( помощь )
5. Sangiorgi, Davide (1993). «От π-исчисления к π-исчислению высшего порядка — и обратно». В Gaudel, M. -C.; Jouannaud, J. -P. (ред.). TAPSOFT'93: Теория и практика разработки программного обеспечения . Конспект лекций по информатике. Том 668. Springer Berlin Heidelberg. стр. 151–166. doi : 10.1007/3-540-56610-4_62 . ISBN 9783540475989.
6. Мазуркевич, Антони (1995). «Введение в теорию следов». В Diekert, V.; Rozenberg, G. (ред.). Книга следов . Сингапур: World Scientific. стр. 3–41. ISBN 981-02-2058-8. Архивировано из оригинала (PostScript) 2011-06-13 . Получено 2009-04-29 .

Дальнейшее чтение

• Мэтью Хеннесси : Алгебраическая теория процессов , Издательство Массачусетского технологического института , ISBN 0-262-08171-7 . 
• К. А. Хоар : Взаимодействие последовательных процессов , Prentice Hall , ISBN 0-13-153289-8 .  
  • Эту книгу обновил Джим Дэвис из Вычислительной лаборатории Оксфордского университета , и новое издание доступно для загрузки в виде файла PDF на веб-сайте Using CSP .
• Робин Милнер : Исчисление коммуникационных систем , Springer Verlag, ISBN 0-387-10235-3 . 
• Робин Милнер : Коммуникационные и мобильные системы: исчисление числа Пи , Springer Verlag, ISBN 0-521-65869-1 . 
• Валк, Рюдигер ; Молдт, Дэниел; Кёлер-Бюссмайер, Михаэль, ред. (2011). «Глава 5: Prozessalgebra - Parallele und kommunizierende Prozesse» (PDF) . Formale Grundlagen der Informatik II: Modellierung und Analyse von Informatiksystemen (на немецком языке). Том. Часть 2. Гамбургский университет . ФГИ2. Архивировано (PDF) из оригинала 9 июля 2019 г. Проверено 13 июля 2019 г. {{cite book}}: |work=проигнорировано ( помощь )