Исчисление общающихся систем

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

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

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

Синтаксис

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

$P ::= \emptyset\,\,\, | \,\,\,a.P_1\,\,\, | \,\,\,A\,\,\, | \,\,\,P_1+P_2\,\,\, | \,\,\,P_1|P_2\,\,\, | \,\,\,P_1[b/a]\,\,\, | \,\,\,P_1{\backslash}a\,\,\,$

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

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

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

действие 

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

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

пишем $A \overset{\underset{\mathrm{def}}{}}{=} P_1$ для использования идентификатора A, чтобы ссылаться на процесс P₁

выбор 

процесс P₁ + P₂ может продолжаться либо как P₁, либо как P₂

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

процессы P₁ и P₂, существующие одновременно

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

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

ограничение 

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

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

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

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

• Исчисление широковещательных систем
• Язык спецификации темпорального упорядочивания (LOTOS)

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

• Моноид истории
• Модель акторов

Ссылки

• 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-131-15007-3. 1989

1. ↑ Tackling Large State Spaces in Performance Modelling // Formal Methods for Performance Evaluation — Springer, 2007. — Т. 4486. — P. 318–370.