Исчисление коммуникационных систем

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

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

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

Синтаксис

Учитывая набор имен действий, набор процессов CCS определяется следующей грамматикой BNF :

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

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

неактивный процесс

неактивный процесс является допустимым процессом CCS ${\displaystyle 0}$

действие

процесс может выполнить действие и продолжиться как процесс ${\displaystyle a.P_{1}}$ ${\displaystyle a}$ ${\displaystyle P_{1}}$

идентификатор процесса

написать , чтобы использовать идентификатор для ссылки на процесс (который может содержать сам идентификатор , т.е. рекурсивные определения разрешены) ${\displaystyle A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}}$ ${\displaystyle A}$ ${\displaystyle P_{1}}$ ${\displaystyle A}$

суммирование

процесс может протекать либо как процесс , либо как процесс ${\displaystyle P_{1}+P_{2}}$ ${\displaystyle P_{1}}$ ${\displaystyle P_{2}}$

параллельная композиция

${\displaystyle P_{1}|P_{2}}$говорит о том, что процессы и существуют одновременно ${\displaystyle P_{1}}$ ${\displaystyle P_{2}}$

переименование

${\displaystyle P_{1}[b/a]}$это процесс со всеми действиями, названными переименованными как ${\displaystyle P_{1}}$ ${\displaystyle a}$ ${\displaystyle b}$

ограничение

${\displaystyle P_{1}{\backslash }a}$это процесс без действия ${\displaystyle P_{1}}$ ${\displaystyle a}$

Связанные исчисления, модели и языки

• Коммуникационные последовательные процессы (CSP), разработанные Тони Хоаром , представляют собой формальный язык, возникший в то же время, что и CCS.
• Алгебра взаимодействующих процессов (ACP) была разработана Яном Бергстрой и Яном Виллемом Клопом в 1982 году и использует аксиоматический подход (в стиле универсальной алгебры ) для рассуждений о классе процессов, подобном CCS.
• Пи -исчисление , разработанное Робином Милнером , Иоахимом Парроу и Дэвидом Уокером в конце 80-х годов, расширяет возможности CCS за счет мобильности каналов связи, позволяя процессам самостоятельно сообщать имена каналов связи.
• Разработанная Джейн Хиллстон модель PEPA вводит хронометраж активности с точки зрения экспоненциально распределенных показателей и вероятностного выбора, что позволяет оценивать показатели производительности.
• Обратимые взаимодействующие параллельные системы (RCCS), представленные Винсентом Даносом, Джин Кривин и другими, вводят (частичную) обратимость в выполнение процессов CCS.

Некоторые другие языки на основе CCS:

• Расчет систем вещания
• Спецификация языка временного упорядочения (LOTOS)
• Исчисление процессов для пространственно-явных экологических моделей (PALPS) является расширением CCS с вероятностным выбором, местоположениями и атрибутами для местоположений ^[2]
• Механизм интерпретатора языка оркестровки Java (Jolie) ^[3]

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

• История моноида
• Модель актера

Ссылки

• Робин Милнер: Исчисление коммуникационных систем , Springer Verlag, ISBN  0-387-10235-3 . 1980.
• Робин Милнер, «Связь и параллелизм» , Prentice Hall, Международная серия по информатике, ISBN 0-13-115007-3 . 1989 

1. Herzog, Ulrich, ed. (май 2007). "Tackling Large State Spaces in Performance Modelling". Формальные методы оценки производительности . Lecture Notes in Computer Science. Vol. 4486. Springer. pp. 318–370. doi :10.1007/978-3-540-72522-0. ISBN 978-3-540-72482-7. Архивировано из оригинала 2008-04-12 . Получено 2009-04-21 .
2. Филиппу А., Торо М., Антонаки М. Моделирование и проверка в исчислении процессов для пространственно-явных экологических моделей. Научные анналы компьютерной науки 23 (1). 2014
3. Монтеси, Фабрицио; Гвиди, Клаудио; Лукки, Роберто; Заваттаро, Джанлуиджи (2007-06-27). "JOLIE: Java Orchestration Language Interpreter Engine". Электронные заметки по теоретической информатике . Объединенные труды Второго международного семинара по координации и организации (CoOrg 2006) и Второго международного семинара по методам и инструментам для координации параллельных, распределенных и мобильных систем (MTCoord 2006). 181 : 19–33. doi : 10.1016/j.entcs.2007.01.051 . ISSN  1571-0661.