Исчисление взаимодействующих систем. Исчисление взаимодействующих систем, ccs, исчисление общающихся систем
Скачать 75.75 Kb.
|
Исчисление взаимодействующих систем (, CCS, исчисление общающихся систем ) в информатике — исчисление процессов, разра- ботанное Робином Милнером в 1980 году. Исчисление работает с моделью неразделяемых коммуникаций между ровно двумя участниками. Фор- мальный язык включает примитивы для описания параллельной ком- позиции, выбора между действиями и рамки ограничений. CCS полезен для оценки качественной корректности свойств таких как взаимная бло- кировка или «живая блокировка». Согласно Милнеру, «нет ничего канонического в выборе базовых ком- бинаторов, даже несмотря на то, что они были выбраны с большим вни- манием к экономии. То, что характеризует наше исчисление, это не точ- ный выбор комбинаторов, но выбор интерпретации и математической структуры”». Выражения языка интерпретируются как помеченная переходная си- стема. Между этими моделями взаимное подобие используется как се- мантическая эквивалентность. Синтаксис Для данного множества имён действий, множество CCS-процессов определяется следующей грамматикой Бэкуса — Наура: P ::= ∅ | a.P 1 | A | P 1 + P 2 | P 1 |P 2 | P 1 [b/a] | P 1 \a Части синтаксиса в данном выше порядке: процесс P 1 с действиями a переименованными в b ограничение : P 1 \a процесс P 1 без действия a] Схожие исчисления и модели • , CSP — язык, разработанный Энтони Хоаром, который появился в то же время, что и CCS. • Пи-исчисление, разработанное Милнером в конце 80-х, предостав- ляет подвижность коммуникационных звеньев, позволяя процессам сообщать имена самих коммуникационных каналов. • Алгебра процессов PEPA, разработанная Джейн Хиллстон, вводит время действия и вероятностный выбор, позволяя вычислять мет- рики производительности. Некоторые нотации, основанные на CCS: • • LOTOS. Модели, которые используются в изучении CCS-систем: • • Модель акторов. |