Исчисление взаимодействующих систем

Исчисление взаимодействующих систем (Шаблон:Lang-en, CCS, исчисление общающихся систем) в информатике — исчисление процессов, разработанное Робином Милнером в 1980 году. Исчисление работает с моделью неразделяемых коммуникаций между ровно двумя участниками. Формальный язык включает примитивы для описания параллельной композиции, выбора между действиями и рамки ограничений. CCS полезен для оценки качественной корректности свойств таких как взаимная блокировка или «живая блокировка».

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

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

Синтаксис

Для данного множества имён действий, множество CCS-процессов определяется следующей грамматикой Бэкуса — Наура:

$P::=\mathrm{\varnothing }|a.P_1|A|P_1+P_2|P_1|P_2|P_1[b/a]|P_1\mathrm{\setminus }a$

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

пустой процесс

пустой процесс $\mathrm{\varnothing }$ — это валидный CCS-процесс

действие

процесс $a.P_1$ может совершать действие $a$ и продолжиться как процесс $P_1$

идентификатор процесса

пишем $A\stackrel{\mathrm{d}\mathrm{e}\mathrm{f}}{=}{P}_1$ для использования идентификатора $A$, чтобы ссылаться на процесс $P_1$

выбор

процесс $P_1+P_2$ может продолжаться либо как $P_1$, либо как $P_2$

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

процессы $P_1$ и $P_2$, существующие одновременно

переименование

$P_1[b/a]$ процесс $P_1$ с действиями $a$ переименованными в $b$

ограничение

$P_1\mathrm{\setminus }a$ процесс $P_1$ без действия $a$

Схожие исчисления и модели

• Шаблон:Не переведено 2, CSP — язык, разработанный Энтони Хоаром, который появился в то же время, что и CCS.
• Пи-исчисление, разработанное Милнером в конце 80-х, предоставляет подвижность коммуникационных звеньев, позволяя процессам сообщать имена самих коммуникационных каналов.
• Алгебра процессов PEPA, разработанная Джейн Хиллстон, вводит время действия и вероятностный выбор, позволяя вычислять метрики производительности.

Некоторые нотации, основанные на CCS:

• Шаблон:Не переведено 2;
• LOTOS.

Модели, которые используются в изучении CCS-систем:

• Шаблон:Не переведено 2;
• Модель акторов.

Ссылки

• Robin Milner: A Calculus of Communicating Systems, Springer Verlag, ISBN 0-387-10235-3. 1980.
• Robin Milner, Communication and Concurrency, Prentice Hall, International Series in Computer Science, ISBN 0-13-115007-3. 1989