|
Título: P-SPADES un algebra de procesos para modelar sistemas de tiempo estocasticos Marco de Trabajo: INVESTIGACION Área de desarrollo: Métodos Formales Autor: Gerardo Saiz Contacto: gsaiz@fing.edu.uy Día: JUEVES Hora: 17:00:00 Palabras Claves: Algebra de Procesos, Probabilidad, Tiempo, Prioridades Resumen: En este trabajo presentamos P-SPADES un algebra de procesos estocastica (SPA) que permite el modelado de sistemas temporales con prioridades y urgencia. Definimos la semantica de P-SPADES en terminos de Automatas Estocasticos con Prioridades (PSA), una extension de automatas, que cuenta con eventos temporizados prioridades y transiciones probabilisticas simbolicas. Los PSA's son objetos simbolicos que tienen una semantica concreta en sistemas de transicion temporizados probabilisticos (PTTS). Por lo tanto P-SPADES tiene semantica concreta en dos pasos en terminos de PTTS. Esto genera dos criterios de equivalencia para procesos en el Algebra definida, estos son bisimulacion simbolica (sobre PSA) y concreta (sobre PTTS). Probamos que los operadores del algebra son definidos de tal modo que ambas bisimulaciones son congruencia con respecto a ellos. Por ultimo se da una axiomatizacion correcta y completa del Algebra con respecto a la bisimulacion simbolica. |
| Ultima modificacion 5 de Octubre 2004 16:30 |