Las lógicas modales surgieron originalmente en el ámbito de la filosofía para responder a limitaciones de la lógica estándar. Sin embargo, rápidamente encontraron aplicación en las ciencias de la computación y actualmente se encuentran presenten en áreas como la teoría de la concurrencia, la verificación y especificación de programas y la representación del conocimiento para inteligencia artificial, entre otras. En los últimos años, las técnicas surgidas de la interacción entre lógica y computación se empiezan a aplicar también en otras ciencias. Destacan las versiones de lenguajes lógicos modales desarrolladas para teoría de juegos, la representación de procesos biológicos con álgebras de procesos y lógicas asociadas a estas álgebras, y la verificación de modelos en la genética. Este proyecto tiene dos objetivos principales: (a) desarrollar y perfeccionar lógicas modales para formalizar el flujo de conocimiento y los efectos de las acciones de los agentes cognoscitivos; (b) aplicar estas lógicas para modelar fenómenos en teoría de juegos, en computación concurrente y paralela y en sistemas biológicos. El punto de partida serán los lenguajes lógicos dinámico-epistémicos propuestos por algunos de los participantes en el pasado. Esperamos que la aplicación combinada de técnicas existentes y de estas nuevas lógicas permita resolver problemas en las áreas anteriormente mencionadas.

Las lógicas modales existentes se han utilizado para resolver problemas en áreas tan diversas como la teoría de la concurrencia o la teoría de juegos. Sin embargo, el área de aplicación posible es mucho más vasta. En particular, este proyecto se plantea modelar: 1. Situaciones donde el intercambio de información y las acciones de agentes independientes tienen un papel fundamental (como en teoría de juegos). 2. La corrección y el desempeño de patrones de software. 3. Procesos biológicos. Para esto, no basta con aplicar enfoques lógicos ya existentes. En este proyecto se trabajará en la modelación de juegos como el dominó, para el cual hay lenguajes que formalizan sólo algunos aspectos, pero no la totalidad del juego. Este tarea requerirá la formulación de axiomas específicos de la lógica dinámica epistémica, la creación de un lenguaje que dé cuenta de las estrategias posibles en el juego y su integración en un sistema computacionalmente eficiente. Se han propuesto lógicas que formalizan algunos tipos de intercambio de información y de acciones. Pero otras clases de intercambio y acciones no están cubiertas por estas lógicas. En particular, está el caso de acciones basadas en el cálculo Pi asíncrono. Los participantes en el proyecto se proponen dar una fundamentación semántica rigurosa a una versión preliminar que presentaron en el pasado reciente. Además, se plantean dotar esta lógica de un sistema de inferencia axiomático y de un mecanismo de verificación de modelos. Los patrones de software son ya una técnica consolidada para la búsqueda de soluciones a problemas computacionales complejos. La idea central es aprovechar las características comunes a diversos problemas que pueden llevar a soluciones que son esencialmente iguales. Hay una gran cantidad de patrones reconocidos por los científicos de la computación, pero la demostración de que poseen las propiedades deseadas se basa sobre todo en razonamientos semi formales sujetos a error. En cuanto a la evaluación del desempeño de estos patrones, es común utilizar simulaciones ad hoc cuya validez no es clara en todas los casos. Este proyecto se propone aplicar métodos algebraicos y lógicos para formalizar patrones conocidos y, de esta manera, demostrar que cumplen con las propiedades deseadas. Las representaciones algebraicas que se usarán permitirán también evaluar su desempeño de manera más formal, lo que a su vez permitirá definir con precisión las condiciones necesarias para que un patrón de software dado sea una solución satisfactoria a un problema específico. Finalmente, se buscará ampliar el campo de aplicación del álgebra de procesos y de las lógicas asociadas a éstas a nuevos fenómenos biológicos. En especial, hay aspectos de la interacción entre genes de una misma red que podrían explicarse de esta manera. Un aspecto de interés particular será la búsqueda de estructuras modulares en una red genética.