Cálculo de sistemas comunicantes

El cálculo de sistemas comunicantes ( CCS ) es un cálculo de procesos introducido por Robin Milner alrededor de 1980 y que da título a un libro que lo describe. Sus acciones modelan comunicaciones indivisibles entre exactamente dos participantes. El lenguaje formal incluye primitivas para describir la composición paralela, la suma entre acciones y la restricción de alcance. El CCS es útil para evaluar la corrección cualitativa de propiedades de un sistema, como el interbloqueo o el bloqueo mutuo . ^{[ 1 ]}

Según Milner, «No hay nada canónico en la elección de los combinadores básicos, aunque se eligieron con gran atención a la economía. Lo que caracteriza nuestro cálculo no es la elección exacta de los combinadores, sino más bien la elección de la interpretación y del marco matemático».

Las expresiones del lenguaje se interpretan como un sistema de transición etiquetado . Entre estos modelos, la bisimilitud se utiliza como una equivalencia semántica.

Dado un conjunto de nombres de acciones, el conjunto de procesos CCS se define mediante la siguiente gramática BNF :

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

Las partes de la sintaxis son, en el orden dado anteriormente

proceso inactivo

el proceso inactivo${\displaystyle 0}$es un proceso CCS válido

acción

el proceso${\displaystyle a.P_{1}}$puede realizar una acción${\displaystyle a}$y continuar como el proceso${\displaystyle P_{1}}$

identificador de proceso

definir${\displaystyle A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}}$y luego usar el identificador${\displaystyle A}$para referirse al proceso${\displaystyle P_{1}}$(que puede contener el identificador)${\displaystyle A}$en sí mismo, es decir, se permiten definiciones recursivas)

suma

el proceso${\displaystyle P_{1}+P_{2}}$puede proceder de cualquiera de las dos maneras.${\displaystyle P_{1}}$o el proceso${\displaystyle P_{2}}$

composición paralela

${\displaystyle P_{1}|P_{2}}$dice que los procesos${\displaystyle P_{1}}$y${\displaystyle P_{2}}$coexistir simultáneamente

cambio de nombre

${\displaystyle P_{1}[b/a]}$es el proceso${\displaystyle P_{1}}$con todas las acciones nombradas${\displaystyle a}$renombrado como${\displaystyle b}$

restricción

${\displaystyle P_{1}{\backslash }a}$es el proceso${\displaystyle P_{1}}$sin acción${\displaystyle a}$

• El lenguaje de comunicación de procesos secuenciales (CSP, por sus siglas en inglés), desarrollado por Tony Hoare , es un lenguaje formal que surgió casi al mismo tiempo que el CCS (Comunicación de Sistemas Comunicativos).
• El Álgebra de Procesos Comunicativos (ACP, por sus siglas en inglés) fue desarrollada por Jan Bergstra y Jan Willem Klop en 1982, y utiliza un enfoque axiomático (al estilo del álgebra universal ) para razonar sobre una clase de procesos similar a la de CCS.
• El cálculo pi , desarrollado por Robin Milner , Joachim Parrow y David Walker a finales de los años 80, amplía la CCS con movilidad de enlaces de comunicación, al permitir que los procesos comuniquen los nombres de los propios canales de comunicación.
• PEPA , desarrollado por Jane Hillston , introduce la sincronización de actividades en términos de tasas distribuidas exponencialmente y elección probabilística, lo que permite evaluar las métricas de rendimiento.
• Los sistemas concurrentes comunicantes reversibles (RCCS, por sus siglas en inglés), introducidos por Vincent Danos , Jean Krivine y otros, introducen la reversibilidad (parcial) en la ejecución de los procesos CCS.

Otros idiomas basados ​​en CCS:

• Cálculo de sistemas de radiodifusión
• Lenguaje de especificación de ordenación temporal (LOTOS)
• El cálculo de procesos para modelos ecológicos espacialmente explícitos (PALPS) es una extensión de CCS con elección probabilística, ubicaciones y atributos para ubicaciones ^{[ 2 ].}
• Motor intérprete del lenguaje de orquestación de Java (Jolie) ^{[ 3 ]}

Modelos que se han utilizado en el estudio de sistemas similares a CCS:

• Historia monoide
• Actor y modelo

• Robin Milner: Un cálculo de sistemas de comunicación , Springer Verlag, ISBN 0-387-10235-31980.
• Robin Milner, Comunicación y concurrencia , Prentice Hall, Serie internacional en ciencias de la computación, ISBN 0-13-115007-31989