Исчисление процессов

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

Основные функции

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Скрытие

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

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

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

$!P=P\mid !P$

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

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

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

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

История

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

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

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

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

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

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

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

• КАПР
• Инструментальные средства параллелизма
• набор инструментов mCRL2

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

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

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

См. также

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

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

• Мэтью Хеннесси : Алгебраическая теория процессов , MIT Press , ISBN   0-262-08171-7 .
• КАР Хоар : Связь последовательных процессов , Прентис Холл , ISBN   0-13-153289-8 .
  • Эта книга была обновлена ​​Джимом Дэвисом из вычислительной лаборатории Оксфордского университета , а новое издание доступно для загрузки в виде PDF- файла на веб-сайте using CSP .
• Робин Милнер : Исчисление коммуникационных систем , Springer Verlag, ISBN   0-387-10235-3 .
• Робин Милнер : Коммуникационные и мобильные системы: Пи-исчисление , Springer Verlag, ISBN   0-521-65869-1 .
• Валк, Рюдигер ; Молдт, Дэниел; Кёлер-Бусмайер, Михаэль, ред. (2011). «Глава 5: Алгебра процессов — параллельные и взаимодействующие процессы» (PDF) . Формальные основы информатики II: моделирование и анализ компьютерных систем (на немецком языке). Том 2. Гамбургский университет . ФГИ2. Архивировано (PDF) из оригинала 9 июля 2019 г. Проверено 13 июля 2019 г. {{cite book}}: |work= игнорируется ( помогите )