Sobre la decidibilidad de dos fragmentos del π-cálculo asincrónico

Resumen

En (Cacciagrano, et al., 2008) se estudió la expresividad de la persistencia en el π-cálculo asincrónico, Aπ. Endicho artículo, los autores consideraron Aπ y tres de sus fragmentos, cada uno de ellos capturando una fuente depersistencia: el fragmento con entradas persistentes (PIAπ), el fragmento con salidas persistentes (POAπ), y elfragmento con tanto entradas como salidas persistentes (PAπ). Ellos demostraron que, bajo ciertas condicionesgenerales, no puede existir una codificación desde Aπ en alguno de sus fragmentos preservando la semántica musttesting,una semántica sensible a la divergencia.En este artículo se ratifican y fortalecen los resultados de separación de (Cacciagrano, et al., 2008) mostrandoque tanto convergencia como divergencia son propiedades decidibles en un fragmento significativo de POAπ yen PAπ., a diferencia de lo que sucede en Aπ. Así, se establece formalmente la no existencia de una codificación(decidable) de Aπ en PAπ o en el fragmento de POAπ, preservando divergencia y convergencia. Estos resultadosde separación no requieren de ninguna condición específica sobre las codificaciones e involucran directamenteconvergencia por primera vez en el estudio de la persistencia de Aπ.