Cálculo de sistemas comunicativos

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

Según Milner, "no hay nada canónico en la elección de los combinadores básicos, aunque se hayan elegido teniendo en cuenta 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 bisimilaridad se utiliza como equivalencia semántica.

Sintaxis

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}\,\,\,|\,\,\,A\,\,\,|\,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_{1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a\,\,\,}$

Las partes de la sintaxis están, en el orden indicado anteriormente

proceso inactivo

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

acción

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

identificador de proceso

escribir para utilizar el identificador para referirse al proceso (que puede contener el identificador mismo, es decir, se permiten definiciones recursivas) ${\displaystyle A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}}$ ${\displaystyle A}$ ${\displaystyle P_{1}}$ ${\displaystyle A}$

suma

El proceso puede continuar como proceso o como proceso. ${\displaystyle P_{1}+P_{2}}$ ${\displaystyle P_{1}}$ ${\displaystyle P_{2}}$

composición paralela

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

cambio de nombre

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

restricción

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

Cálculos, modelos y lenguajes relacionados

• La comunicación de procesos secuenciales (CSP), desarrollado por Tony Hoare , es un lenguaje formal que surgió en una época similar a la del CCS.
• El Álgebra de Procesos de Comunicación (ACP) 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 similar de procesos al CCS.
• El cálculo pi , desarrollado por Robin Milner , Joachim Parrow y David Walker a finales de los años 80, extiende el CCS con la movilidad de los 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 cronología de la actividad en términos de tasas distribuidas exponencialmente y elección probabilística, lo que permite evaluar métricas de rendimiento.
• Los sistemas concurrentes comunicantes reversibles (RCCS), introducidos por Vincent Danos, Jean Krivine y otros, introducen reversibilidad (parcial) en la ejecución de procesos CCS.

Algunos otros idiomas basados ​​en CCS:

• Cálculo de sistemas de radiodifusión
• Especificación del lenguaje de ordenamiento temporal (LOTOS)
• El cálculo de procesos para modelos ecológicos espacialmente explícitos (PALPS) es una extensión del CCS con elección probabilística, ubicaciones y atributos para las ubicaciones ^[2]
• Motor de interpretación del lenguaje de orquestación Java (Jolie) ^[3]

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

• Historial monoide
• Modelo de actor

Referencias

• Robin Milner: Un cálculo de sistemas de comunicación , Springer Verlag, ISBN  0-387-10235-3 . 1980.
• Robin Milner, Comunicación y concurrencia , Prentice Hall, Serie internacional en informática, ISBN 0-13-115007-3 . 1989 

1. Herzog, Ulrich, ed. (mayo de 2007). "Abordaje de grandes espacios de estados en el modelado del rendimiento". Métodos formales para la evaluación del rendimiento . Notas de clase en informática. Vol. 4486. Springer. págs. 318–370. doi :10.1007/978-3-540-72522-0. ISBN 978-3-540-72482-7Archivado desde el original el 12 de abril de 2008. Consultado el 21 de abril de 2009 .
2. A Philippou, M Toro, M Antonaki. Simulación y verificación en un cálculo de procesos para modelos ecológicos espacialmente explícitos. Scientific Annals of Computer Science 23 (1). 2014
3. Montesi, Fabrizio; Guidi, Claudio; Lucchi, Roberto; Zavattaro, Gianluigi (27 de junio de 2007). "JOLIE: un motor intérprete del lenguaje de orquestación Java". Notas electrónicas en informática teórica . Actas combinadas del Segundo taller internacional sobre coordinación y organización (CoOrg 2006) y el Segundo taller internacional sobre métodos y herramientas para coordinar sistemas concurrentes, distribuidos y móviles (MTCoord 2006). 181 : 19–33. doi : 10.1016/j.entcs.2007.01.051 . ISSN  1571-0661.