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

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

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

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

Синтаксис

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

P ::= ∅ | a . P 1 | A | P 1 + P 2 | P 1 | P 2 | P 1 [ b / a ] | P 1 ∖ a {displaystyle P::=emptyset ,,,|,,,a.P_{1},,,|,,,A,,,|,,,P_{1}+P_{2},,,|,,,P_{1}|P_{2},,,|,,,P_{1}[b/a],,,|,,,P_{1}{ackslash }a}

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

пустой процесс пустой процесс ∅ {displaystyle emptyset } — это валидный CCS-процесс действие процесс a . P 1 {displaystyle a.P_{1}} может совершать действие a {displaystyle a} и продолжиться как процесс P 1 {displaystyle P_{1}} идентификатор процесса пишем A = d e f P 1 {displaystyle A{overset {underset {mathrm {def} }{}}{=}}P_{1}} для использования идентификатора A {displaystyle A} , чтобы ссылаться на процесс P 1 {displaystyle P_{1}} выбор процесс P 1 + P 2 {displaystyle P_{1}+P_{2}} может продолжаться либо как P 1 {displaystyle P_{1}} , либо как P 2 {displaystyle P_{2}} параллельная композиция процессы P 1 {displaystyle P_{1}} и P 2 {displaystyle P_{2}} , существующие одновременно переименование P 1 [ b / a ] {displaystyle P_{1}[b/a]} процесс P 1 {displaystyle P_{1}} с действиями a {displaystyle a} переименованными в b {displaystyle b} ограничение P 1 ∖ a {displaystyle P_{1}{ackslash }a} процесс P 1 {displaystyle P_{1}} без действия a {displaystyle a}

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

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

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

• Исчисление широковещательных систем (англ. Calculus of Broadcasting Systems);
• LOTOS.

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

• Моноид истории (англ. History monoid);
• Модель акторов.