Las redes genéticas son idealizaciones por medio de las cuales los biólogos tratan de sintetizar la interacción entre distintos genes en un organismo. Aunque son un vehículo muy sintético para concentrar el resultado de múltiples experimentos, en el caso de redes relativamente complejas es muy difícil el extraer información más general por limitaciones computacionales: ¿la red alcanzará alguna vez un estado estacionario?, ¿cuántos estados estacionarios existen?, ¿hay estados que se repitan cíclicamente? ¿la red es robustez ante diversos tipos de perturbaciones o asincronía y estocasiticidad?, etc Por esta razón, existe un enorme interés en la aplicación de técnicas que permitan plantear y resolver las cuestiones anteriores de la manera más directa y eficiente posible. Varias de estas técnicas surgieron del área de verificación de modelos en lógica, en particular con lenguajes lógicos modales. La verificación de modelos (y la aplicación de la lógica en general) ya ha obtenido varios resultados atractivos para los biólogos (lo que se refleja en un número creciente de investigadores en esta línea), pero aún existen retos considerables relacionados (entre otras cuestiones) con la expresividad de los lenguajes utilizados, la eficiencia computacional de los métodos de verificación y la facilidad de plantear y responder las preguntas de interés para los biólogos que utilizan las redes genéticas. Nuestro proyecto abordará estos retos utilizando tanto técnicas existentes (algunas desarrolladas por nosotros) como otras nuevas, que nos planteamos crear o adaptar de otras áreas de la lógica.

Las contribuciones principales del proyecto serán a) el desarrollo de lenguajes lógicos más expresivos en términos de propiedades de redes genéticas, con el costo computacional mínimo posible; b) mayor eficiencia computacional para la obtención de información a partir de las redes genéticas formalizadas en nuestros modelos; c) un marco conceptual y una interfaz más accesible a los biólogos, los usuarios finales, los cuales no suelen estar familiarizados con los formalismos lógicos; d) un sistema en línea mejorado que, partiendo de los logros de Antelope (un verificador de modelos basado en CTL desarrollado por algunos de los participantes en el proyecto [Arellano et al., 2011]), incorpore lo anterior.