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

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

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

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

СинтаксисПравить

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

\text{[math]}

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

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

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

Схожие исчисления и моделиПравить

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

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

Модели, которые используются в изучении 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-13-115007-3. 1989

↑ Tackling Large State Spaces in Performance Modelling // Formal Methods for Performance Evaluation (англ.) / Herzog, Ulrich. — Springer, 2007. — Vol. 4486. — P. 318—370. — (Lecture Notes in Computer Science). — doi:10.1007/978-3-540-72522-0.

[1] Tackling Large State Spaces in Performance Modelling // Formal Methods for Performance Evaluation (англ.) / Herzog, Ulrich. — Springer, 2007. — Vol. 4486. — P. 318—370. — (Lecture Notes in Computer Science). — doi:10.1007/978-3-540-72522-0.

[1]