Máquina de estados finitos comunicante

Para un entero positivo arbitrario${\displaystyle N}$, un protocolo ^{[ 1 ] : 3} con${\displaystyle N}$El/los proceso(s) es(son) cuádruple(s)${\displaystyle \{(S_{i})_{i=1}^{N},\ (o_{i})_{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^{N}\}}$con:

• ${\displaystyle (S_{i})_{i=1}^{N}}$, una secuencia de${\displaystyle N}$conjuntos finitos disjuntos. Cada conjunto se utiliza para representar un proceso, y cada elemento de${\displaystyle S_{i}}$representa un posible estado de la${\displaystyle i}$-º proceso.
• ${\displaystyle (o_{i})_{i=1}^{N}}$(con${\displaystyle o_{i}\in S_{i}}$), una secuencia que representa el estado inicial de cada proceso.
• ${\displaystyle (M_{i,j})_{i,j=1}^{N}}$, una secuencia finita de${\displaystyle N^{2}}$conjuntos finitos disjuntos tales que cada conjunto${\displaystyle M_{i,j}}$representa los posibles mensajes que pueden enviarse desde el proceso${\displaystyle i}$procesar${\displaystyle j}$. Si${\displaystyle i=j}$, entonces${\displaystyle M_{i,j}}$está vacío.
• ${\displaystyle ({\mathtt {succ}})_{i=1}^{N}:S_{i}\times \bigcup _{j=1}^{N}\left(M_{j,i}^{[+]}\cup M_{i,j}^{[-]}\right)\mapsto S_{i}}$es una secuencia de funciones de transición. Cada función modela la transición que se puede tomar al emitir o recibir cualquier mensaje. Con respecto al proceso${\displaystyle i}$, el símbolo${\displaystyle [+]}$se utiliza para anotar un mensaje que se puede recibir y${\displaystyle [-]}$un mensaje que se puede enviar.

Un estado global es un par${\displaystyle \langle S,C\rangle }$dónde

• ${\displaystyle S=(s_{1},...,s_{N})}$es una colección ordenada de estados tal que cada${\displaystyle s_{i}}$representa un estado de la${\displaystyle i}$-º proceso.
• ${\displaystyle C}$es un${\displaystyle N\times N}$matriz tal que cada${\displaystyle c_{i,j}\in C}$es una subsecuencia de${\displaystyle M_{i,j}}$.

El estado global inicial es un par${\displaystyle \langle O,\mathrm {E} \rangle }$dónde

• ${\displaystyle O=(o_{1},...,o_{N})}$
• ${\displaystyle \mathrm {E} }$se define como un${\displaystyle N\times N}$matriz tal que para todo${\displaystyle i,j\in \{1,...,N\}}$,${\displaystyle E_{i,j}}$es igual a la palabra vacía,${\displaystyle \epsilon }$.

Existen dos tipos de pasos: pasos en los que se reciben mensajes y pasos en los que se envían mensajes.

Un paso en el que el${\displaystyle j}$El proceso recibe un mensaje enviado previamente por el${\displaystyle i}$El proceso -ésimo es un par de la forma ${\displaystyle \left\langle (s_{1},\dots ,s_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }$cuando${\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}}$, con${\displaystyle m'_{i,j}\in M_{i,j}}$. De manera similar, un par en el que se envía un mensaje por el${\displaystyle i}$-º proceso al${\displaystyle j}$-el uno es un par de la forma ${\displaystyle \left\langle (s_{1},\dots ,s_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }$cuando ${\displaystyle {\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}}$

Una ejecución es una secuencia de estados globales tal que un paso relaciona un estado con el siguiente, y tal que el primer estado es el inicial.

Se dice que un estado global${\displaystyle \langle S,C\rangle }$es alcanzable si existe una ejecución que pase por este estado.

Se ha demostrado, con la introducción del concepto mismo, que cuando dos máquinas de estados finitos se comunican con un solo tipo de mensaje, se pueden determinar e identificar la acotación, los interbloqueos y el estado de recepción no especificado, mientras que esto no ocurre cuando las máquinas se comunican con dos o más tipos de mensajes. Posteriormente, se ha demostrado además que cuando solo una máquina de estados finitos se comunica con un único tipo de mensaje, mientras que la comunicación de su compañera no está restringida, aún podemos determinar e identificar la acotación, los interbloqueos y el estado de recepción no especificado. ^{[ 2 ]}

Se ha demostrado además que cuando la relación de prioridad de mensajes está vacía, se pueden decidir la acotación, los interbloqueos y el estado de recepción no especificado incluso bajo la condición en la que hay dos o más tipos de mensajes en la comunicación entre máquinas de estados finitos. ^{[ 4 ]}

La acotación, los interbloqueos y el estado de recepción no especificado son todos decidibles en tiempo polinomial (lo que significa que un problema particular puede resolverse en una cantidad de tiempo manejable, no infinita) ya que los problemas de decisión relacionados con ellos son completos en el espacio logarítmico no determinista. ^{[ 2 ]}

Un sistema de canales es esencialmente una versión de una máquina de estados finitos comunicante en la que la máquina no está dividida en procesos distintos. Por lo tanto, existe un único estado de estado y no hay restricciones sobre qué sistema puede leer o escribir en un canal determinado.

Formalmente, dado un protocolo${\displaystyle \langle (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},(M_{i,j})_{i,j=1}^{n},({\mathtt {succ}})_{i}\rangle }$, su sistema de canales asociado es${\displaystyle \langle \prod (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},\bigcup _{i,j=1}^{n}(M_{i,j}),\Delta \rangle }$, dónde${\displaystyle \Delta }$es el conjunto de${\displaystyle ((s_{1},\dots ,s_{j},\dots ,s_{n}),?m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{j}(s_{j},+m_{i,j}),\dots ,s_{n})}$y de${\displaystyle ((s_{1},\dots ,s_{i},\dots ,s_{n}),!m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{i}(s_{i},-m_{i,j}),\dots ,s_{n})}$.