Tpbcun cálculo sobre redes de Petri con tiempo

Résumé

En el trabajo se realiza un estudio exhaustivo de una extensión con tiempo de PBC (Petri Box Calculus), que es un modelo formal de especificación de sistemas concurrentes en el que se da especial importancia a la sincronización y el paralelismo, y cuya semántica denotacional utiliza como soporte redes de Petri. La Tesis comienza con la exposición detallada de un modelo básico para el que se define una semántica operacional, formada por un conjunto de relgas de transición al estilo Plotkin, y una semántica denotacional, que genera un álgebra de redes de Petri temporizadas. A continuación se introducen los elementos necesarios para incorporar la urgencia en la ejecución de dichas acciones, y al estudio de un nuevo operador, denominado time-out con excepción, que permite el establecimiento de ocmportamientos alternativos. La urgencia de los procesos, característica imprescindible en la modelización de sistemas temporizados reales, se refuerza con una tercera modificación en la que se incorpora el máximo paralelismo, que facilita la ejecución más rápida posible de las acciones de una expresión de proceso. El resultado técnico fundamental del trabajo es la equivalencia entre las semánticas operacional y denontacional del modelo definido, en el sentido de que ambas definen comportamientos equivalentes para cada expresión. Durante todo el análisis, el dominio de tiempo considerado es discreto, pues de esta forma se consiguen importantes simplifaciones, que nos conducen a un modelo más tratable pero suficientemente expresivo. La Tesis se completa con los resultados obtenidos sobre una segunda extensión de PBC que incorpora al Cálculo de Cajas el concepto de ambiente de Cardelli, tratando satisfactoriamente los aspectos relativos a la movilidad. Ello representa una vía de ampliación del modelo básico que incorpora a su semátncia operacional reglas equivalentes a las que definen el Cálculo de Ambientes, y cuya