CSP Probabilístico (PCSP)un modelo operacional

Resumen

Presentamos un álgebra de procesos para la modelización de procesos comunicantes probabilísticos. El tipo de álgebra es asíncrono, al igual que los modelos clásicos, y contrariamente a la mayoría de álgebras probabilísticas estudiadas hasta el momento (PCCS), que son síncronicas. La principal dificultad en nuestro modelo proviene de disponer en el mismo de dos tipos de elección (interna y externa), al contrario que en los anteriores, donde sólo existe uno. Otra dificultad, que nuestro modelo no alcanza a resolver el el funcionamiento del operador de ocultamiento. Si queremos mantener su significado clásico, necesitaríamos añadir más potencia a nuestra semántica. Definiremos una semántica operacional del lenguaje, y la usaremos para razonar sobre su potencia mediante un ejemplo no trivial, en el que mostraremos la posibilidad de modelizar propiedades como la seguridad (reliabibity), y el cálculo de tiempos medios (performance).