Исчисление коммуникационных систем

Исчисление коммуникационных систем ( CCS ) — это исчисление процессов, введенное Робином Милнером примерно в 1980 году, и название книги, описывающей это исчисление. Его действия моделируют неделимые коммуникации ровно между двумя участниками. Формальный язык включает примитивы для описания параллельной композиции, выбора между действиями и ограничения области действия. CCS полезен для оценки качественной корректности свойств системы, таких как взаимоблокировка или активная блокировка . ^[1]

По словам Милнера, «в выборе основных комбинаторов нет ничего канонического, хотя они были выбраны с большим вниманием к экономии. Наше исчисление характеризует не точный выбор комбинаторов, а скорее выбор интерпретации и математической основы». ".

Выражения языка интерпретируются как обозначенная система переходов . Между этими моделями бисходство используется как семантическая эквивалентность.

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

Учитывая набор имен действий, набор процессов CCS определяется следующей грамматикой BNF :

P::=0\,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_{1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a\,\,\,

Части синтаксиса в порядке, указанном выше:

неактивный процесс: неактивный процесс $0$ это действительный процесс CCS
действие: процесс $a.P_{1}$ может выполнить действие $a$ и продолжайте процесс $P_{1}$
идентификатор процесса: писать $A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}$ использовать идентификатор $A$ ссылаться на процесс $P_{1}$ (который может содержать идентификатор $A$ само по себе, т. е. допускаются рекурсивные определения)
суммирование: процесс $P_{1}+P_{2}$ может продолжаться либо как процесс $P_{1}$ или процесс $P_{2}$
параллельная композиция: $P_{1}|P_{2}$ сообщает, что процессы $P_{1}$ и $P_{2}$ существовать одновременно
переименование: $P_{1}[b/a]$ это процесс $P_{1}$ со всеми названными действиями $a$ переименован в $b$
ограничение: $P_{1}{\backslash }a$ это процесс $P_{1}$ без действий $a$

, модели и Связанные языки исчисления

Коммуникационные последовательные процессы (CSP), разработанные Тони Хоаром , представляют собой формальный язык, возникший одновременно с CCS.
Алгебра коммуникативных процессов (ACP) была разработана Яном Бергстрой и Яном Виллемом Клопом в 1982 году и использует аксиоматический подход (в стиле универсальной алгебры ) для рассуждений о классе процессов, аналогичном CCS.
Пи -исчисление , разработанное Робином Милнером , Джоахимом Пэрроу и Дэвидом Уокером в конце 80-х годов, расширяет CCS мобильностью каналов связи, позволяя процессам самим сообщать названия каналов связи.
PEPA , разработанный Джейн Хиллстон, представляет время активности с точки зрения экспоненциально распределенных ставок и вероятностного выбора, что позволяет оценивать показатели производительности.
Реверсивные коммуникационные параллельные системы (RCCS), представленные Винсентом Даносом , Жаном Кривином и другими, вводят (частичную) обратимость при выполнении процессов CCS.

Некоторые другие языки на основе CCS:

Расчет систем вещания
Спецификация языка временного упорядочения (LOTOS)
Исчисление процессов для пространственно-явных экологических моделей (PALPS) представляет собой расширение CCS с вероятностным выбором, местоположениями и атрибутами мест. ^[2]
Механизм интерпретации языка оркестровки Java (Jolie) ^[3]

Модели, которые использовались при исследовании CCS-подобных систем:

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

Робин Милнер: Исчисление коммуникационных систем , Springer Verlag, ISBN 0-387-10235-3 . 1980.
Робин Милнер, Коммуникации и параллелизм , Прентис Холл, Международная серия по информатике, ISBN 0-13-115007-3 . 1989 год

^ Герцог, Ульрих, изд. (май 2007 г.). «Решение больших пространств состояний в моделировании производительности» . Формальные методы оценки эффективности . Конспекты лекций по информатике. Том. 4486. Спрингер. стр. 318–370. дои : 10.1007/978-3-540-72522-0 . ISBN 978-3-540-72482-7 . Архивировано из оригинала 12 апреля 2008 г. Проверено 21 апреля 2009 г.
^ Филиппу, Торо, Антонаки. Моделирование и проверка в расчете процессов для пространственно-явных экологических моделей.Научные анналы информатики 23 (1). 2014 год
^ Монтези, Фабрицио; Гуиди, Клаудио; Лукки, Роберто; Заваттаро, Джанлуиджи (27 июня 2007 г.). «JOLIE: механизм интерпретации языка оркестровки Java» . Электронные заметки по теоретической информатике . Объединенные материалы второго международного семинара по координации и организации (CoOrg 2006) и второго международного семинара по методам и инструментам координации параллельных, распределенных и мобильных систем (MTCoord 2006). 181 : 19–33. дои : 10.1016/j.entcs.2007.01.051 . ISSN 1571-0661 .

[1] Герцог, Ульрих, изд. (май 2007 г.). «Решение больших пространств состояний в моделировании производительности» . Формальные методы оценки эффективности . Конспекты лекций по информатике. Том. 4486. Спрингер. стр. 318–370. дои : 10.1007/978-3-540-72522-0 . ISBN 978-3-540-72482-7 . Архивировано из оригинала 12 апреля 2008 г. Проверено 21 апреля 2009 г.

[2] Филиппу, Торо, Антонаки. Моделирование и проверка в расчете процессов для пространственно-явных экологических моделей.Научные анналы информатики 23 (1). 2014 год

[3] Монтези, Фабрицио; Гуиди, Клаудио; Лукки, Роберто; Заваттаро, Джанлуиджи (27 июня 2007 г.). «JOLIE: механизм интерпретации языка оркестровки Java» . Электронные заметки по теоретической информатике . Объединенные материалы второго международного семинара по координации и организации (CoOrg 2006) и второго международного семинара по методам и инструментам координации параллельных, распределенных и мобильных систем (MTCoord 2006). 181 : 19–33. дои : 10.1016/j.entcs.2007.01.051 . ISSN 1571-0661 .

[1]

[2]

[3]

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