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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Исчисление взаимодействующих систем (англ. Calculus of Communicating Systems, CCS, исчисление общающихся систем) в информатике — исчисление процессов, разработанное Робином Милнером в 1980 году. Исчисление работает с моделью неразделяемых коммуникаций между ровно двумя участниками. Формальный язык включает примитивы для описания параллельной композиции, выбора между действиями и рамки ограничений. CCS полезен для оценки качественной корректности свойств таких как взаимная блокировка или «живая блокировка»[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_1 может совершать действие a и продолжиться как процесс P_1
идентификатор процесса 
пишем A \overset{\underset{\mathrm{def}}{}}{=} 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{\backslash}a процесс P_1 без действия a

Схожие исчисления и модели[править | править вики-текст]

Некоторые нотации, основанные на 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
  1. Tackling Large State Spaces in Performance Modelling // Formal Methods for Performance Evaluation. — Springer, 2007. — Vol. 4486. — P. 318–370.