Una coinstitución para la lógica de comportamiento abstracto

Resumen

Recientemente, la especificación de un problema en ciencias de la computación –un paso intermedio entre el problema dado y su aplicación como un sistema de software que garantiza su solución– utiliza el álgebra universal y la teoría de coálgebras para su descripción. Esta etapa incluye componentes sintácticas y semánticas, que tienen como resultado un sistema lógico. En [3], se propone la lógica ecuacional multitipada para la especificación de problemas. Dualmente, en [9] se estudia una lógica de comportamiento abstracto, la cual modela procesos y comportamiento de sistemas coalgebraicos. En ambas lógicas los componentes sintáctico y semántico son conectados por medio de una relación de satisfacción, caracterizada por el siguiente principio: la verdad se preserva bajo transformaciones del lenguaje. En un marco general y moderno, hoy contamos con las instituciones en la especificación algebraica y coinstituciones en la especificación coalgebraica. El propósito del presente artículo es estudiar un caso particular de la lógica de comportamiento abstracto presentada en [9], en donde las coálgebras las restringimos a funtores polinomiales. Identificamos la respectiva coinstitución coalgebraica, detallando sus componentes y explícitamente presentaremos la relación de satisfacción como un resultado final.

Para citar este artículo: J.A. Castaño Perea, G. Ortiz Rico, Una coinstitución para la lógica de comportamiento abstracto, Rev. Integr. Temas Mat. 32 (2014), no. 2, 199-210.