SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA

2016

MINISTERIO DE ECONOMIA Y COMPETITIVIDAD

INV. COMPETITIVA PROYECTOS

Escobar Román Santiago

Para abordar los retos requeridos por los sistemas software actuales, son necesarias soluciones efectivas. Muchos retos en Tecnología Informática para la Sociedad Digital suponen el análisis de sistemas complejos, p.ej. problemas de planificación en fábricas inteligentes, análisis de recursos y seguridad en sistemas distribuidos, problemas de protección en programas multihilo, asignación dinámica de recursos en sistemas en la nube, etc. Estos sistemas interdependientes y complejos están cada vez más presentes en ciudades inteligentes, en el área de sanidad pública, o en el transporte sostenible. Muchos de estos sistemas dependen de propiedades de seguridad y protección vitales para la economía. Sin embargo, la creación de herramientas robustas para analizarlos es todavía un hito significativo. Nuestra aproximación para obtener soluciones eficientes se centra en los siguientes pasos: (1) un sistema complejo y real se representa con un modelo abstracto; (2) los problemas se expresan en un determinado marco lógico y; (3) se aplican potentes tecnologías basadas en la lógica para analizar y resolver los problemas. El proyecto LoBaSS contribuye en las tres direcciones: modelar problemas reales, expresar problemas en marcos lógicos y desarrollar técnicas y herramientas para solucionarlos u optimizarlos. La aproximación en conjunto permite aplicar las mismas técnicas a distintos dominios (p.ej. computación en la nube, fábricas inteligentes, análisis de protocolos de comunicaciones), haciendo el desarrollo de herramientas para resolver problemas reales más sencillo y rápido. Como base del proyecto utilizaremos extensiones y combinaciones de la lógica proposicional, de primer orden y estructuras algebraicas. En concreto, consideraremos: SAT (satisfacción de fórmulas proposicionales), SMT (SAT módulo teorías), programación con restricciones (CP), lógica difusa (FL), lógica de reescritura (RWL), programación lógica (LP), programación inductiva (IP) e interpretación abstracta (AI). En este proyecto, nos centraremos en la combinación y extensión de estos lenguajes formales para obtener la expresividad necesaria en nuestras aplicaciones prácticas. Nos guiaremos por los retos actuales en Tecnología Informática para planificación, seguridad, aprendizaje automático, análisis de sistemas complejos, bio-informática o manipulación de XML, así como para el desarrollo de algoritmos y herramientas eficientes para generar y resolver los problemas descritos. Como aplicaciones concretas, consideramos: (a) planificación de actividades deportivas con KNVB, Holanda, (b) optimización y planificación en colaboración con Barcelogic Solutions y el interés de compañías como SIMO y E2F, (c) análisis de sistemas complejos en colaboración con Microsoft Research en Cambridge y el interés de compañías como IBM, Thales, Clearsy, Vossloh, Edicom y Semantic Systems, (d) seguridad en colaboración con la Universidad de Illinois en Urbana-Champaign y el Laboratorio de la Marina en Washington, (e) planificación difusa de recursos en centros de datos en la nube con la Universidad de Umea y (f) evaluación de secuencias de transcripción en colaboración con el Instituto Hospital del Mar de Investigaciones Médicas (IMIM). Nuestro proyecto cubre todas las etapas de desarrollo y aplicación de tecnologías informáticas, desde la teoría básica hasta los retos actuales en tecnologías de la información para la sociedad digital y el transporte inteligente, integrado y sostenible.