Исчисление взаимодействующих систем
Исчисление взаимодействующих систем (англ. Calculus of Communicating Systems, CCS, исчисление общающихся систем) в информатике — исчисление процессов, разработанное Робином Милнером в 1980 году. Исчисление работает с моделью неразделяемых коммуникаций между ровно двумя участниками. Формальный язык включает примитивы для описания параллельной композиции, выбора между действиями и рамки ограничений. CCS полезен для оценки качественной корректности свойств таких как взаимная блокировка или «живая блокировка»[1].
Согласно Милнеру, «нет ничего канонического в выборе базовых комбинаторов, даже несмотря на то, что они были выбраны с большим вниманием к экономии. То, что характеризует наше исчисление, это не точный выбор комбинаторов, но выбор интерпретации и математической структуры».
Выражения языка интерпретируются как помеченная переходная система. Между этими моделями взаимное подобие используется как семантическая эквивалентность.
Синтаксис
Для данного множества имён действий, множество CCS-процессов определяется следующей грамматикой Бэкуса — Наура:
- [math]\displaystyle{ P ::= \emptyset\,\,\, | \,\,\,a.P_1\,\,\, | \,\,\,A\,\,\, | \,\,\,P_1+P_2\,\,\, | \,\,\,P_1|P_2\,\,\, | \,\,\,P_1[b/a]\,\,\, | \,\,\,P_1{\backslash}a }[/math]
Части синтаксиса в данном выше порядке:
- пустой процесс
- пустой процесс [math]\displaystyle{ \emptyset }[/math] — это валидный CCS-процесс
- действие
- процесс [math]\displaystyle{ a.P_1 }[/math] может совершать действие [math]\displaystyle{ a }[/math] и продолжиться как процесс [math]\displaystyle{ P_1 }[/math]
- идентификатор процесса
- пишем [math]\displaystyle{ A \overset{\underset{\mathrm{def}}{}}{=} P_1 }[/math] для использования идентификатора [math]\displaystyle{ A }[/math], чтобы ссылаться на процесс [math]\displaystyle{ P_1 }[/math]
- выбор
- процесс [math]\displaystyle{ P_1+P_2 }[/math] может продолжаться либо как [math]\displaystyle{ P_1 }[/math], либо как [math]\displaystyle{ P_2 }[/math]
- параллельная композиция
- процессы [math]\displaystyle{ P_1 }[/math] и [math]\displaystyle{ P_2 }[/math], существующие одновременно
- переименование
- [math]\displaystyle{ P_1[b/a] }[/math] процесс [math]\displaystyle{ P_1 }[/math] с действиями [math]\displaystyle{ a }[/math] переименованными в [math]\displaystyle{ b }[/math]
- ограничение
- [math]\displaystyle{ P_1{\backslash}a }[/math] процесс [math]\displaystyle{ P_1 }[/math] без действия [math]\displaystyle{ a }[/math]
Схожие исчисления и модели
- Исчисление взаимодействующих процессов (англ. 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.