n veces a través del espejo

Abstract

Este trabajo se enfoca en el área de semántica de sistemas reactivos que, a diferencia de los sistemas relaciónales o funcionales, se caracterizan por mantener una interacción con el ambiente. Sobre dichos sitemas se define una gran clase de operadores unarios, cuyos representantes típicos son los operadores de prioridad, de renombrado y de ocultamiento y se estudia su compatibilidad con respecto a equivalencias semánticas en modelos de si.stem.as de transiciones etiquetadas (STE). En principio se consideran los operadores de prioridad y se obtiene que la n-nested. simulación no es una congruencia para ellos. Se muestra que la m.a.yor congruencia. contenida en esta equivalencia es estrictamente más gruesa que la n + 1-nested simulación. Luego se generaliza el conjunto de operadores para incluir muchos de los operadores unarios estáticos usados en sistemas reactivos y se obtiene que ready-simulación y bisimulación son congruencias para ese conjunto. Se demuestra además que la n- nested sim.ulación es una congruencia sólo cuando el operador unario es monótono. Finalmente se introduce una nueva familia infinita de equivalencias semánticas sobre los STE, la n-nested ready simulación que posee las propiedades requeridas de congruencia para todos los operadores de la clase estudiada. Esta familia es estrictamente más fina que la mayor congruencia para estos operadores que está contenida en la n-nested simulación.