Tesis (Ciencias de la Computación e Inteligencia Artificial)

URI permanente para esta colecciónhttps://hdl.handle.net/11441/11305

Examinar

Envíos recientes

Mostrando 1 - 20 de 35
  • EmbargoTesis Doctoral
    Virus machines: an unconventional computing paradigm
    (2024-05-28) Ramírez de Arellano Marrero, Antonio; Orellana Martín, David; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    Sobrepasar la estructura convencional de los ordenadores actuales diseñada John von Neumann desde hace casi 100 años es uno de los grandes retos de las ciencias de la computación. Existen enfoques teóricos para abarcar este problema, uno de ellos consiste en desarrollar paradigmas de computación no convencionales inspirados en la naturaleza, a esta disciplina se le llama Computación Natural. En esta no sólo se desarrollan modelos prácticos para diversas aplicaciones, sino que también da otro enfoque al desarrollo de teorías de complejidad computacional a través de estos modelos. Es común que, al desarrollar un nuevo paradigma de computación, esta sufra de ciertas carencias matemáticas en pro de buscar aplicaciones directas del mismo. Lo que realmente da un salto cualitativo a estos nuevos modelos es una buena base construida desde la integridad matemática, no sólo para buscar aplicaciones, sino que también para atacar problemas abstractos. En esta tesis se desarrolla un joven paradigma de computación llamado Máquinas de Virus, el cual se inspira en la propagación y replicación de los virus biológicos. En la tesis se aplica una técnica de verificación formal para dar veracidad matemática a los distintos ejemplos prácticos que se plantean en la misma, entre ellos se encuentran diversos modos, computación de funciones, generador de conjuntos, y aceptación de problemas de decisión. Llegando a atacar criptosistemas con estas máquinas. Por último, se definen diversas extensiones del paradigma para mejorar la eficiencia y también buscar aplicaciones al mundo real con modelos basados en estos. Se concluye que este paradigma de computación ofrece un enfoque interesante y que, al compararlo con otros bien establecidos basados en las redes neuronales, se puede llegar a mejores resultados en términos de universalidad y diferenciados para aplicaciones prácticas.
  • Acceso AbiertoTesis Doctoral
    Multi-omics characterization of the responses to seasonal variations in diel cycles in the marine picoeukaryote ostreococcus tauri
    (2024-03-08) Romero Losada, Ana Belén; García González, Mercedes; Romero Campero, Francisco José; Universidad de Sevilla. Departamento de Bioquímica Vegetal y Biología Molecular; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    Earth tilted rotation and translation around the Sun produce one of the most pervasive periodic environmental signals on our planet giving rise to seasonal variations in diel cycles. Marine phytoplankton undergo significant alterations in response to these signals and, although it plays a key role on ecosystems, their response to these rhythms remains largely unexplored. In this work, the marine picoalga Ostreococcus tauri is chosen as model organism grown under summer long days, winter short days, constant light and constant dark conditions to characterize these responses. The 80 % of its transcriptome present diel rhythmicity and genes with robust self-sustained rhythmic expression profiles are identified. A drastic reduction in proteome rhythmicity with respect to transcriptome rhythmicity is observed with 25 % of the proteins oscillating. Seasonally specific rhythms are found in key physiological processes such as cell cycle, photosynthesis, carotenoid biosynthesis, starch accumulation and nitrate assimilation. A global orchestration between transcriptome, proteome and physiological dynamics is observed with specific seasonal temporal offsets between gene expression, protein abundance levels and physiological activity.
  • Acceso AbiertoTesis Doctoral
    Control del reloj circadiano por la señal fotoperiódica en plantas
    (2022-04-28) Reyes Rodríguez, Pedro de los; Romero Rodríguez, José María; Romero Campero, Francisco José; Valverde Albacete, Federico; Universidad de Sevilla. Departamento de Bioquímica Vegetal y Biología Molecular; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    Los organismos fotosintéticos son muy eficientes en la adaptación de su desarrollo a las condiciones ambientales. Para conseguir esta adaptación monitorizan continuamente los estímulos externos que les llegan del ambiente y promueven cambios fisiológicos, como ocurre con las modificaciones del transcriptoma. La luz solar es esencial para la supervivencia de los organismos fotosintéticos, ya que constituye su principal fuente de energía y controla múltiples aspectos de su fisiología. En la percepción de la luz en plantas y algas participan un conjunto de receptores y factores de transcripción que conectan las señales procedentes de la luz con cambios específicos en la expresión génica. La existencia de eventos externos cíclicos muy predecibles como la sucesión de días/noches o de las estaciones, permite coordinar y anticipar de manera muy robusta los procesos biológicos. Esta medida del tiempo es llevada a cabo por un oscilador interno denominado reloj circadiano. Por otra parte, la señalización de la vía fotoperiódica permite a los organismos vegetales medir la longitud del día y así obtener información estacional para controlar complejos procesos que son clave para su supervivencia como la floración. Uno de los genes centrales en esta vía es CONSTANS, que está regulado a nivel transcripcional y postraduccional por el reloj circadiano y por señales luminosas. En esta tesis doctoral se ha seguido un enfoque de Biología Molecular de Sistemas para entender cómo han evolucionado estos procesos a lo largo del linaje verde, se han generado herramientas para su estudio y finalmente se ha descrito una nueva conexión entre el reloj circadiano y la vía fotoperiódica en la planta modelo Arabidopsis thaliana. En una primera aproximación investigamos la evolución de la expresión génica diaria en el linaje vegetal, empleando las microalgas Ostreococcus tauri y Chlamydomonas reinhardtii y la planta superior Arabidopsis thaliana. Inicialmente, realizamos un estudio de ortología que ha revelado por una parte la aparición de genes específicos en Chamydomonas y Arabidopsis y por otra parte la amplificación y diversificación de familias génicas. Además, hemos investigado cómo ha cambiado la influencia de los ciclos día/noche sobre el transcriptoma a lo largo de la evolución vegetal mediante la construcción de redes de co-expresión en ciclos de luz/oscuridad. Nuestros resultados indican una mayor dependencia de los ciclos diurnos en microalgas que en plantas. En cuanto a la evolución de los patrones de expresión, hemos observado un alto nivel de conservación en genes que se expresan en las transiciones luz/oscuridad a pesar de la gran distancia evolutiva entre algas y plantas. Estos resultados pueden ser explorados en la herramienta CircadiaNet. En segundo lugar, construimos la red transcripcional ATTRACTOR que integra datos transcriptómicos y datos de ChIP-seq de factores de transcripción involucrados en el reloj circadiano y en la señalización por luz. De esta forma, el estudio de la red permite investigar la regulación coordinada del reloj circadiano y la señalización lumínica sobre la expresión génica en Arabidopsis. Mediante el análisis topológico de ATTRACTOR hemos descrito que estos programas transcripcionales poseen la característica conocida como “robusto pero frágil”, es decir, son robustos frente a ataques aleatorios y frágiles frente a ataques dirigidos a genes altamente conectados. Por otra parte, se ha demostrado que los genes cuya regulación es más dependiente del reloj circadiano se expresan durante las primeras horas de la mañana, modulando procesos concretos como respuesta inmune, respuesta a hormonas o crecimiento. Además, se ha descrito que algunos motivos de red compuestos por varios factores de transcripción pueden explicar la regulación de determinados aspectos del desarrollo, dando lugar a propiedades emergentes. Por ejemplo, el motivo formado por CCA1, PIF y PRR5 participa en la respuesta a sequía y frío. Para este fin, se ha desarrollado una aplicación web para su exploración por parte de la comunidad científica. Por último, utilizando estas herramientas, hemos demostrado un nuevo papel para CO en la regulación del reloj circadiano en Arabidopsis. CO formaría parte de una señalización retrógrada desde la vía fotoperiódica hacia el oscilador central, proporcionando información estacional al reloj. En condiciones de día largo, CO se une a genes centrales del reloj circadiano para alterar su perfil de expresión. Uno de estos genes es el PSEUDO RESPONSE REGULATOR 5 (PRR5), con el que además comparte sitios de unión en el genoma. Por ello, CO y PRR5 establecen un motivo de doble retroalimentación con salida múltiple regulando genes diana en común. Además, hemos encontrado que CO se une a motivos de DNA G-box en estos promotores, probablemente a través del factor de transcripción bZIP LONG HYPOCOTIL 5 (HY5).
  • Acceso AbiertoTesis Doctoral
    Promoting and inhibiting contexts in membrane computing
    (2005-11-29) Sburlan, Dragos; Paun, Gheorghe; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
  • Acceso AbiertoPremio Extraordinario de Doctorado USTesis Doctoral
    Membrane computing, neural inspirations, gene assembly in ciliates
    (2007-03-28) Ishdorj, Tseren-Onolt; Paun, Gheorghe; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    La Tesis enmarca dentro de la disciplina de la computación celular con membranas, un modelo de computación orientado a máquinas, inspirado en la estructura y funcionamiento de las células de los organismos vivos, Que fue creada por G. Paun a finales de 1998 y que, en Octubre de 2003, el prestigioso institute for scientific information (I.S.I., USA) designó a dicha disciplina como fast emergin research front in computes science. La memoria aporta nuevas vías para atacar una serie de problemas clásicos relativos a la potencia y la eficiencia computacional de modelos de computación bio-inspirados y no convencionales, así como resultados relevantes en dichos modelos, conformando una memoria de gran valor científico que cumple, con creces, los requisitos para ser considerados como una tesis doctoral con acreditación de doctorado europeo.
  • Acceso AbiertoPremio Extraordinario de Doctorado USTesis Doctoral
    Optimization of high-throughput real-time processes in physics reconstruction
    (2019-11-29) Cámpora Pérez, Daniel Hugo; Riscos Núñez, Agustín; Neufeld, Niko; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    La presente tesis se ha desarrollado en colaboración entre la Universidad de Sevilla y la Organización Europea para la Investigación Nuclear, CERN. El detector LHCb es uno de los cuatro grandes detectores situados en el Gran Colisionador de Hadrones, LHC. En LHCb, se colisionan partículas a altas energías para comprender la diferencia existente entre la materia y la antimateria. Debido a la cantidad ingente de datos generada por el detector, es necesario realizar un filtrado de datos en tiempo real, fundamentado en los conocimientos actuales recogidos en el Modelo Estándar de física de partículas. El filtrado, también conocido como High Level Trigger, deberá procesar un throughput de 40 Tb/s de datos, y realizar un filtrado de aproximadamente 1 000:1, reduciendo el throughput a unos 40 Gb/s de salida, que se almacenan para posterior análisis. El proceso del High Level Trigger se subdivide a su vez en dos etapas: High Level Trigger 1 (HLT1) y High Level Trigger 2 (HLT2). El HLT1 transcurre en tiempo real, y realiza una reducción de datos de aproximadamente 30:1. El HLT1 consiste en una serie de procesos software que reconstruyen lo que ha sucedido en la colisión de partículas. En la reconstrucción del HLT1 únicamente se analizan las trayectorias de las partículas producidas fruto de la colisión, en un problema conocido como reconstrucción de trazas, para dictaminar el interés de las colisiones. Por contra, el proceso HLT2 es más fino, requiriendo más tiempo en realizarse y reconstruyendo todos los subdetectores que componen LHCb. Hacia 2020, el detector LHCb, así como todos los componentes del sistema de adquisici´on de datos, serán actualizados acorde a los últimos desarrollos técnicos. Como parte del sistema de adquisición de datos, los servidores que procesan HLT1 y HLT2 también sufrirán una actualización. Al mismo tiempo, el acelerador LHC será también actualizado, de manera que la cantidad de datos generada en cada cruce de grupo de partículas aumentare en aproxidamente 5 veces la actual. Debido a las actualizaciones tanto del acelerador como del detector, se prevé que la cantidad de datos que deberá procesar el HLT en su totalidad sea unas 40 veces mayor a la actual. La previsión de la escalabilidad del software actual a 2020 subestim´ó los recursos necesarios para hacer frente al incremento en throughput. Esto produjo que se pusiera en marcha un estudio de todos los algoritmos tanto del HLT1 como del HLT2, así como una actualización del código a nuevos estándares, para mejorar su rendimiento y ser capaz de procesar la cantidad de datos esperada. En esta tesis, se exploran varios algoritmos de la reconstrucción de LHCb. El problema de reconstrucción de trazas se analiza en profundidad y se proponen nuevos algoritmos para su resolución. Ya que los problemas analizados exhiben un paralelismo masivo, estos algoritmos se implementan en lenguajes especializados para tarjetas gráficas modernas (GPUs), dada su arquitectura inherentemente paralela. En este trabajo se dise ˜nan dos algoritmos de reconstrucción de trazas. Además, se diseñan adicionalmente cuatro algoritmos de decodificación y un algoritmo de clustering, problemas también encontrados en el HLT1. Por otra parte, se diseña un algoritmo para el filtrado de Kalman, que puede ser utilizado en ambas etapas. Los algoritmos desarrollados cumplen con los requisitos esperados por la colaboración LHCb para el año 2020. Para poder ejecutar los algoritmos eficientemente en tarjetas gráficas, se desarrolla un framework especializado para GPUs, que permite la ejecución paralela de secuencias de reconstrucción en GPUs. Combinando los algoritmos desarrollados con el framework, se completa una secuencia de ejecución que asienta las bases para un HLT1 ejecutable en GPU. Durante la investigación llevada a cabo en esta tesis, y gracias a los desarrollos arriba mencionados y a la colaboración de un pequeño equipo de personas coordinado por el autor, se completa un HLT1 ejecutable en GPUs. El rendimiento obtenido en GPUs, producto de esta tesis, permite hacer frente al reto de ejecutar una secuencia de reconstrucción en tiempo real, bajo las condiciones actualizadas de LHCb previstas para 2020. As´ı mismo, se completa por primera vez para cualquier experimento del LHC un High Level Trigger que se ejecuta únicamente en GPUs. Finalmente, se detallan varias posibles configuraciones para incluir tarjetas gr´aficas en el sistema de adquisición de datos de LHCb.
  • Acceso AbiertoTesis Doctoral
    El problema P versus NP: desarrollo de nuevas técnicas a través de modelos de computación bio-inspirados.
    (2019-04-01) Orellana Martín, David; Pérez Jiménez, Mario de Jesús; Valencia Cabrera, Luis; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
  • Acceso AbiertoTesis Doctoral
    Descubrimiento de conocimiento en grafos multi-relacionales
    (2017-06-30) Almagro Blanco, Pedro; Sancho Caparrini, Fernando; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    Ante el reducido abanico de metodologías para llevar a cabo tareas de aprendizaje automático relacional, el objetivo principal de esta tesis es realizar un análisis de los métodos existentes, modificando u optimizando en la medida de lo posible algunos de ellos, y aportar nuevos métodos que proporcionen nuevas vías para abordar esta difícil tarea. Para ello, y sin nombrar objetivos relacionados con revisiones bibliográficas ni comparativas entre modelos e implementaciones, se plantean una serie de objetivos concretos a ser cubiertos: 1. Definir estructuras flexibles y potentes que permitan modelar fenómenos en base a los elementos que los componen y a las relaciones establecidas entre éstos. Dichas estructuras deben poder expresar de manera natural propiedades complejas (valores continuos o categóricos, vectores, matrices, diccionarios, grafos,...) de los elementos, así como relaciones heterogéneas entre éstos que a su vez puedan poseer el mismo nivel de propiedades complejas. Además, dichas estructuras deben permitir modelar fenómenos en los que las relaciones entre los elementos no siempre se dan de forma binaria (intervienen únicamente dos elementos), sino que puedan intervenir un número cualquiera de ellos. 2. Definir herramientas para construir, manipular y medir dichas estructuras. Por muy potente y flexible que sea una estructura, será de poca utilidad si no se poseen las herramientas adecuadas para manipularla y estudiarla. Estas herramientas deben ser eficientes en su implementación y cubrir labores de construcción y consulta. 3. Desarrollar nuevos algoritmos de aprendizaje automático relacional de caja negra. En aquellas tareas en las que nuestro objetivo no es obtener modelos explicativos, podremos permitirnos utilizar modelos de caja negra, sacrificando la interpretabilidad a favor de una mayor eficiencia computacional. 4. Desarrollar nuevos algoritmos de aprendizaje automático relacional de caja blanca. Cuando estamos interesados en una explicación acerca del funcionamiento de los sistemas que se analizan, buscaremos modelos de aprendizaje automático de caja blanca. 5. Mejorar las herramientas de consulta, análisis y reparación para bases de datos. Algunas de las consultas a larga distancia en bases de datos presentan un coste computacional demasiado alto, lo que impide realizar análisis adecuados en algunos sistemas de información. Además, las bases de datos en grafo carecen de métodos que permitan normalizar o reparar los datos de manera automática o bajo la supervisión de un humano. Es interesante aproximarse al desarrollo de herramientas que lleven a cabo este tipo de tareas aumentando la eficiencia y ofreciendo una nueva capa de consulta y normalización que permita curar los datos para un almacenamiento y una recuperación más óptimos. Todos los objetivos marcados son desarrollados sobre una base formal sólida, basada en Teoría de la Información, Teoría del Aprendizaje, Teoría de Redes Neuronales Artificiales y Teoría de Grafos. Esta base permite que los resultados obtenidos sean suficientemente formales como para que los aportes que se realicen puedan ser fácilmente evaluados. Además, los modelos abstractos desarrollados son fácilmente implementables sobre máquinas reales para poder verificar experimentalmente su funcionamiento y poder ofrecer a la comunidad científica soluciones útiles en un corto espacio de tiempo.
  • Acceso AbiertoPremio Extraordinario de Doctorado USTesis Doctoral
    Modelado de sistemas dinámicos con MachineLearning: aplicaciones al mantenimiento basado en la condición.
    (2018-02-05) Cabrera Mendieta, Diego Román; Sancho Caparrini, Fernando; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    El estudio de los sistemas dinámicos es un tema de gran interés tanto en la ingeniería como en las ciencias por su gran aplicabilidad a la resolución de problemas que, con frecuencia, aparecen en un sin número de ´áreas. Sin embargo los métodos formales hasta ahora utilizados para su análisis, no han tenido la flexibilidad suficiente para adaptarse a sistemas de complejidad creciente, donde la interacción de sus elementos no permite una inferencia directa del comportamiento del sistema, en una, o varias de sus variables. Por otro lado, los nuevos avances en las técnicas de Machine Learning han demostrado tener una gran capacidad de adaptación en dominios tan diversos resultando en la necesidad de cambios minoritarios para su aplicación entre uno u otro. A pesar de esto, su estudio en el modelado de sistemas dinámicos, como tarea fundamental, ha sido pocas veces abordado. Por las razones anteriores, este trabajo se enfoca en el desarrollo de 3 metodologías para modelado de sistemas dinámicos desde la perspectiva del Machine Learning a partir de información incompleta de sus variables representadas como series temporales de alta complejidad. Las propuestas son presentadas en función de los diferentes escenarios de información disponible para el modelado, que pudieran llegar a aparecer en situaciones reales. Como primera metodología se propone el modelamiento del sistema dinámico con un enfoque manual de caracterización de estados usando el conocimiento a-priori del sistema mediante la descomposición por Wavelet Packet y la posterior identificación de patrones mediante una técnica clásica de clasificación ´on llamada Random Forest. Como segunda propuesta se presenta el aprendizaje no-supervisado del proceso de caracterización que se adapta de forma automática al sistema dinámico en estudio mediante el modelo Stacked Convolucional Autoencoder, el cual inicializa una Red Neuronal Convolucional Profunda que luego es optimizada de forma supervisada, donde además el proceso de identificación de patrones se encuentra embebido, y es optimizado junto con el modelo de extracción de características. La tercera propuesta en cambio cumple la tarea de caracterización de identificación de patrones de forma no-supervisada, lo primero mediante el aprendizaje de una representación óptima de las series temporales codificada en los parámetros de un Echo State Network, y lo segundo por medio de un Variational Autoencoder, un modelo capaz de aproximar la distribución de probabilidad (a menudo compleja) de los datos. En esta última aproximación se elimina la necesidad de conocer la etiqueta de las series de tiempo que provienen de los estados del sistema dinámico. Las metodologías propuestas son evaluadas en tareas de mantenimiento basado en la condición como son el diagnóstico de fallos, la estimación de la severidad de daño y la detección de fallos en elementos de maquinaria rotativa (concretamente distintos tipos de engranajes y rodamientos). Los altos índices de exactitud obtenidos en los resultados de la evaluación en cada tarea, muestran que las metodologías aportadas dan un nivel elevado de confiabilidad, robustez y flexibilidad. Además, frente a comparaciones realizadas con otras metodologías reportadas en el estado del arte, las propuestas presentan un desempeño superior en todos los casos.
  • Acceso AbiertoTesis Doctoral
    Desarrollo y aplicaciones de un entorno de programación para computación celular: P-Lingua
    (2010-06-24) Pérez Hurtado de Mendoza, Ignacio; Pérez Jiménez, Mario de Jesús; Riscos Núñez, Agustín; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    La presente memoria está estructurada en tres partes que constan de un total de siete capítulos cuyos contenidos se describen sucintamente a continuación. Parte I: Preliminares La memoria comienza con un breve recorrido histórico acerca del desarrollo y evolución de diversos conceptos relacionados con la Teoría de la Computación y la Teoría de la Complejidad Computacional. Se analizan las limitaciones que tienen los dispositivos reales construidos en el marco de dichas teorías, a la hora de resolver eficientemente problemas concretos que son relevantes en la vida real, lo cual hace necesario la búsqueda de nuevos paradigmas de computación que permitan superar algunas de esas limitaciones. Se presentan los conceptos básicos de la Computación Natural y, en particular, de la rama de la Computación celular con membranas, Membrane Computing, en la que se enmarcan los trabajos que se presentan en esta memoria. En el Capítulo 2 se analiza la problemática actual relativa a la modelización de procesos complejos de la realidad, justificando la necesidad de utilizar modelos formales a _n de conseguir ciertos avances de tipo cualitativo. Se describen brevemente algunas aproximaciones clásicas, así como otras más recientes de tipo computacional que tratan de capturar la aleatoriedad inherente a los procesos biológicos. Finalmente, se presenta un marco de especificación para el diseño de modelos basados en el paradigma de Membrane Computing. Parte II: Aplicaciones de software en Membrane Computing El Capítulo 3 está dedicado a justificar la necesidad de desarrollar herramientas informáticas para poder analizar la bondad de los modelos computacionales diseñados, a través de una validación experimental basada en simulaciones. Se presenta una breve panorámica de los simuladores de sistemas P desarrollados hasta la fecha y se describen los elementos comunes que tienen todos ellos y que han de ser implementados. En el Capítulo 4 se presenta un entorno de programación para el paradigma de Membrane Computing. Dicho entorno está compuesto de: (a) un lenguaje de programación para la especificación de sistemas P (P-Lingua); (b) una biblioteca que implementa el procesamiento de ficheros y diversos algoritmos de simulación (pLinguaCore); y (c) una serie de herramientas para la línea de comandos. La última parte está dedicada a la presentación de ejemplos de código de distintos sistemas P, incluyendo dos familias que proporcionan soluciones eficientes del problema SAT de la satisfactibilidad de la Lógica Proposicional. Parte III: Aplicación al estudio de ecosistemas reales En el Capítulo 5 se describe un marco específico para la modelización computacional de ecosistemas basado en Membrane Computing. En particular, se presentan las concreciones del marco general para los sistemas P probabilísticos y, además, se describe con detalle un algoritmo de simulación que trata de capturar la semántica probabilística. Además, se presenta el software EcoSim 2.0 que es una familia de herramientas para la simulación de modelos de ecosistemas y que se ha desarrollado utilizando P-Lingua y pLinguaCore. El capítulo finaliza con un ejemplo simple de ilustración acerca de las interacciones tritróficas. El Capítulo 6 está dedicado al diseño de modelos basados en sistemas P de dos ecosistemas reales. El primero de ellos se refiere a un ecosistema de la zona pirenaico-catalana en donde habita una ave carroñera en peligro de extinción, el quebrantahuesos; el segundo está dedicado a la modelización computacional de un ecosistema del pantano de Ribarroja, gestionado por Endesa S.A. en el que una especie exótica invasora (el mejillón cebra) está causando importantes problemas de sostenibilidad del medio ambiente con la destrucción de especies autóctonas, así como graves problemas de tipo económico al provocar importantes destrozos en instalaciones diversas de la compañía en torno a dicho pantano. En ambos casos, se han diseñado sendos modelos basados en sistemas P multientornos funcionales-probabilísticos para los cuales se han desarrollado aplicaciones informáticas ad hoc que permitan la validación experimental de los modelos y su uso para la realización de experimentos virtuales a partir de diferentes escenarios de interés para los expertos. La memoria finaliza con un breve capítulo dedicado a la presentación de conclusiones y líneas de trabajo futuro de investigación.
  • Acceso AbiertoTesis Doctoral
    P systems, a computational modelling framework for systems biology
    (2008-02-06) Romero Campero, Francisco José; Gheorghe, Marian; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    LOS PROGRAMAS INFORMÁTICOS QUE MODELIZAN CÉLULAS FACILITARÁN EL TRABAJO DE LOS BIÓLOGOS Se basa en hacer modelos de células, por lo que llevo tres años en los que estoy realizando modelos de sistemas biológicos en bacterias. Una parte de programación la realizan ingenieros de software, pero yo monto el algoritmo o el modelo que simula el comportamiento de las bacterias y hago el proceso de validac ión de comparación con los datos del biólogo. El lenguaje que utilizan estos modelos de células está muy cerca del que emplean los biólogos y realizar experimentos con modelos de sistemas celulares desde un ordenador es relativamente fácil, en comparación con el esfuerzo de tiempo y dinero que supone elaborar las pruebas necesarias en un laboratorio hasta alcanzar resultados. Los biólogos no están acostumbrados a modelizar y es muy difícil obtener conocimientos del montón de datos que nos proporcionan. Así pues, nosotros intentamos simplificarlos y abstraerlos hasta conseguir un nuevo conocimiento. El modelo que diseñemos se tiene que comportar tal y como los biólogos indican, así ellos podrán trabajar desde un primer momento con nuestros programas para ver cómo funcionan los experimentos desde el ordenador. Una vez que ya lo hayan comprobado podrán saber si es rentable llevarlo al laboratorio.
  • Acceso AbiertoTesis Doctoral
    Modeling and simulation of real-life phenomena in membrane computing
    (2013-10-11) García-Quismondo Fernández, Manuel; Martínez del Amor, Miguel Ángel; Pérez Jiménez, Mario de Jesús; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    This document is structured in three parts, whose content is briefly outlined below. Part I: Preliminaries Chapter I familiarizes the reader with the basics of Natural Computing, introducing some classical models in the discipline. Following, it delves into the state of the art of Membrane Computing. Some frameworks including the seminar transition model are discussed. Finally, it contra sts stochastic and probabilistic approaching when modelling real-life phenomena. Chapter II discusses simulators in Membrane Computing and describes the project P-Lingua and the software tool pLinguaCore, which enable experts to describe and simulate P systems automatically. Moreover, some Membrane Computing simulators implemented on parallel platforms are described, with an special emphasis on those developed for Graphic Processing Units (GPU). Part II: Contributions Chapter III discusses Enzymatic Numerical P Systems (ENPS), a deterministic model for robotics, introducing its antecedents and sequential simulators. In addition, a parallel, GPU-based simulator is presented, including a performance analysis with some case studies and a methodology for repeated simulation of ENPSs. Chapter IV discusses a model on Logic Networks (LNs), which are a specific type of Gene Regulatory Networks in which the combination of the states of a set of genes can influence another one. In addition, a model based on Population Dynamic P systems (PDP systems, for short) is finally presented, describing its semantics and its elements in detail. Chapter V formalizes Probabilistic Guarded P Systems (PGP Systems, for short), a new modelling framework for ecology. The characteristic features of this approach are described, i.e., its spatial distribution and elements and its syntax and semantics. A parallel, GPU-based simulator is described, as well as the integration of PGP systems into the P-Lingua framework. Part III: Results Chapter VI presents some case studies on the models and simulators described in part II, specifically, the modelling and simulation of a Logic Network involved in the flowering process of Arabidopsis thaliana by means of LNDP systems and the modelling and simulation of the ecosystem of White Cabbage Buttery (Pieris napi oleracea). Chapter VII focuses on the results compiled in this document, recapitulating the achievements and conclusions of this thesis and discussing some new lines of work resulting from it.
  • Acceso AbiertoTesis Doctoral
    Especificación y verificación de programas moleculares en PVS
    (2003-09-29) Graciani Díaz, Carmen; Pérez Jiménez, Mario de Jesús; Sancho Caparrini, Fernando; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    La Computación Molecular y, en concreto, la Computación con ADN, es una disciplina que se enmarca dentro del campo de investigación conocido como Computación Natural. Tiene como objetivo el desarrollo de modelos de computación inspirados en el comportamiento de las moléculas de ADN, y en las posibilidades que abren las técnicas de laboratorio para su manipulación. En la memoria se han estudiado distintas adaptaciones del marco formal en que se describen distintos modelos de computación con ADN al lenguaje de especificaciones de PVS, que es un sistema de verificación cuyo lenguaje está basado en la lógica clásica de segundo orden con un sistema de tipos acorde con la teoría de conjuntos de Zermelo-Fraenkel con el axioma de elección. El demostrador del sistema está basado en cálculos de secuentes combinando la interacción con el usuario y el automatismo. Como aportaciones originales señalar la descripción en PVS del modelo restringido de Adleman y el modelo sticker, y la representación y verificación en PVS de programas moleculares que resuelven problemas clásicos NP-completos. En una primera aproximación al modelo sticker se ha realizado una implementación de la metodología presentada por Fernando Sancho en su tesis doctoral para la verificación de programas en el citado modelo. Así mismo, la consideración de los programas en este modelo como meros programas imperativos ha llevado a la descripción de la lógica de primer orden para dos tipos (indpendiente de la del sistema) y del cálculo de Floyd-Hoare, desarrollando un conjunto de estrategias que permiten simi-automatizar el proceso de verificación de programas imperativos. La presente memoria tiene dos objetivos fundamentales: por un lado estudiar la adaptación de nuevos modelos de computación no convencionales al marco formal de un sistema de verificación automática y, por otro, verificar la corrección y completitud de programas en dichos modelos utilizando para ello el demostrados del sistema. En esta memoria se presentan distintas aproximaciones a dos modelos de computación molecular basada en ADN y a la verificación de programas moleculares en los mismos que resuelven algunos problemas clásicos. El desarrollo de la misma está estructurada en capítulos que pasamos a reseñar sucintamente. En el Capítulo 1 se describen algunos paradigmas y modelos de Computación Natural como son las redes neuronales artificiales, los algoritmos genéticos, la programación evolutiva, la computación molecular, y la computación celular, como marco dentro del cual se describen los modelos de computación basados en AD, una de las áreas en la que se desarrolla presente memoria. En el Capítulo 2 se presenta una descripción básica del sistema PVS, con el fin de facilitar la lectura y compresión de los capítulos posteriores sin requerir un conocimiento mayor del mismo. Cada una de las secciones del capítulo se corresponde con uno de los elementos del lenguaje de especificaciones del sistema. Por último se incluye un breve ejemplo que ilustra el manejo del demostrador. El Capítulo 3 está dedicado a la computación molecular basada en ADN. Se incluye una descripción de la estructura química del ADN y su comportamiento, así como de algunas de las técnicas de laboratorio que se utilizan para su manipulación y que justifican la elección de las operaciones elementales de los modelos de computación molecular considerados. Por su importancia histórica se presenta al experimento de Adleman, considerando propiamente el origen de la Computación basada en ADN. Por último, se describen los modelos restringido de Adleman y sticker, objeto de estudio de la presente memoria. El primero como representante de los modelos sin memoria, ya que las operaciones moleculares consideradas no alteran la estructura de las moléculas de ADN. El segundo, como ejemplo de un modelo molecular con memoria, por el uso que hace de las moléculas de ADN como unidades de memoria que pueden ser modificadas a lo largo de la ejecución de un programa. En el Capítulo 4 se presentan, en primer lugar, dos problemas clásicos en teoría de la complejidad computacional, el problema SAT de la satisfactibilidad de la Lógica Proposicional y el problema de la 3 coloración de un grafo no dirigido. El trabajo de F. Martín y otros inspiró la posibilidad de utilizar un demostrador para la implementación y verificación de programas en modelos moleculares. Basado en dicho trabajo se realizó una primera aproximación en PVS basada en listas. A continuación se desarrolló una segunda implementación que utiliza como tipos de datos básicos los multiconjuntos y las sucesiones finitas de elementos, que permiten manejar de manera más natural las estructuras de datos del modelo. Dado que los dos problemas anteriores tienen en común que en el tubo inicial deben estar representadas todas las posibles funciones con dominio un conjunto finito de elementos y rango en un conjunto de valores, se especifica la construcción de un tubo inicial genérico. Por último, se incluye la verificación de programas moleculares diseñados para resolver los problemas citados. En el Capítulo 5 se estudia la implementación de una metodología diseñada por F. Sancho para la verificación de programas en el modelo sticker. Al considerar los programas como una sucesión de instrucciones básicas, éstos se consideran como la composición de funciones elementales. La única peculiaridad la proporcionan los bucles que son tratados como funciones recursivas dependientes de un valor para el caso base y una función que representa la sucesión de instrucciones que se repite a lo largo del bucle. Como ilustración se presente la verificación de una serie de programas moleculares diseñados para resolver problemas relativos a conjuntos numéricos y que son utilizados como subrutinas de programas que resuelven problemas clásicos NP-completos: el problema Subset-Sum, el problema de la Mochila 0/1 acotado, el problema del empaquetamiento, Set Packing¸ el del recubrimiento exacto, Exact Cover, y el problema del recubrimiento minimal. A continuación se puede decir que empieza una segunda parte en la memoria, en la que se consideran los programas en el modelo sticker como meros programas imperativos y, como tales, susceptibles de ser verificados con los métodos habituales utilizados para este tipo de programas, basados en las especificaciones de corrección parcial de Floyd-Hoare. Se considera que la ejecución de un programa imperativo produce un cambio de estado; es decir, un cambio en el valor de las variables asociadas al programa. Para poder expresar los programas y determinados asertos que permitan formular las condiciones de corrección de los mismos, Gloees represente en PVS la lógica clásica de Primer Orden y una técnica de verificación de programas imperativos basada en el cálculo de Hoare. En el capítulo 6 se presenta la lógica clásica y la lógica tipada de Primer Orden. A continuación se describe una implementación de la primera y el desarrollo, en PVS, de una lógica de primer orden para dos tipos, que nos permitirá escribir los programas de modelos sticker y demostrar la corrección de los mismos. En el Capítulo 7 se describe la implementación de las distintos comandos o instrucciones con los que se construyen los programas imperativos considerados: asignaciones, secuenciación y bucles para. Con cada una de las instrucciones consideradas se incluye el esquema o axioma correspondiente de la lógica de Floyd-Hoare que permite establecer la corrección de las mismas. Las operaciones del modelo se consideran como términos en las variables del programa. Para ilustrar el comportamiento de la misma se incluye la especificación de las subrutinas y del programa, presentadas en el capítulo 5, para resolver el problema del recubrimiento exacto en el modelo sticker, estableciendo su corrección. En el último capítulo de esta memoria se resumen algunas de las ideas acerca del desarrollo del trabajo, se presentan algunos datos que permiten cuantificar el mismo y se destaca algunas conclusiones extraídas de los resultados obtenidos. Se concluye con las perspectivas de trabajo futuro que se vislumbran tras los objetivos conseguidos en esta memoria y que marcan una línea de investigación en modelos de computación no convencionales.
  • Acceso AbiertoTesis Doctoral
    Formalización en Isar de la metalógica de primer orden
    (2012-06-12) Serrano Suárez, Fabián Fernando; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. Más precisamente, formalizar en el sistema de razonamiento Isabelle/HOL/Isar la metateoría de la lógica de primer orden como se expone en capítulo 1 del libro "Introduction to mathematical logic" de Elliott Mendelson y en los primeros cinco capítulos del libro "First-Order Logic and Automated Theorem Proving" de M. Fitting. 1) Se presenta una formalización de un sistema axiomático de la lógica proposicional y la demostración de la completitud del sistema usando el método de Kalmar de eliminación de variables. 2) Se presenta una formalización de la terminación y corrección de un algoritmo para calcular una forma normal conjuntiva de una fórmula proposicional. El algoritmo está descrito en términos de la notación uniforme para las fórmulas de la lógica proposicional; para demostrar su terminación se define una función de medida en términos de los conceptos de "multiconjunto" y "rango" de una fórmula. 3) Se formaliza la corrección de un procedimiento de prueba de tautologías usando tableros semánticos. La terminación se demuestra de la misma forma que en el caso del algoritmo de la forma normal conjuntiva. Para la formalización de la completitud de este método de prueba se utiliza el lemma de Hintikka. 4) Se formaliza la demostración del teorema de existencia de modelos para un conjunto consistente S de fórmulas pertenecientes a un lenguaje proposicional L. Esta demostración está basada en extender S a un conjunto consistente maximal M el cual resulta ser satisfacible (por ser un conjunto de Hintikka) y por tanto S también. Como una aplicación del teorema de existencia de modelos en la lógica proposicional, se formalizan el teorema de compacidad y el teorema de interpolación de Craig. 6) Se presenta la formalización de la sintaxis y semántica de la lógica de primer orden. Para la representación de las fórmulas se emplea la notación de de Bruijn y se formaliza el teorema de existencia de modelos en la lógica de primer orden siguiendo el mismo orden de ideas que en el caso proposicional, y como una aplicación se formaliza la demostracion del teorema de Löwenheim-Skolem. 7) Por último, se define un sistema de deducción natural para lo lógica de primer orden. Se formaliza su corrección y como una consecuencia del teorema de existencia de modelos para la lógica de primer orden, se formaliza su completitud.
  • Acceso AbiertoTesis Doctoral
    Bordismo seccional de fibrados y submersiones
    (1988-12-16) Arrabal Parrilla, Juan José; Domínguez Murillo, Eladio; Quintero Toscano, Antonio Rafael; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial; Universidad de Sevilla. SEJ189: Estud.estad.e Hist.series Temp.en Andalucia,XIX-XX
    El objeto de este trabajo es sistematizar una técnica que intenta atacar el problema de existencia de secciones de funciones continuas o funciones diferenciables, y el problema de triangulación de una variedad topológica. El antecedente directo de esta técnica está en la teoría de homología seccional introducida por Weshu Shih, para el estudio de los sistemas de ecuaciones diferenciales no lineales. Dada una aplicación contínua f : X →B entre espacios topológicos X y B. Shih consideró el conjunto simplicial K(f) construido como sigue: Los q-símplices son las parejas (σ,γ), donde σ:Δq→B es una aplicación inyectiva continua del q-símplice estándar Δq=((Xo,X1,…,Xq)ЄRq+1|X1≥0, ΣXi=1> en B. y γ es uan función continua γ:Δq→X tal que σ=f•γ. Los operadores cara se definen de una manera natural. Cuando X, B son variedades diferenciales, f es un morfismo diferenciable y KЄZ+U(∞), se define el subconjunto simplicial K(f)k de K(f) formado por las (σ,γ) diferenciables de clase Ck, con σ inmersión difeomorfa (fr. “plongement”). Entonces definió el grupo de homología seccional con soportes propios de f. designado por H*(f)s, como el grupo de homología de las cadenas localmente finitas del conjunto simplicial K(f) con coeficientes enteros. De la misma manera definió los grupos seccionales H*(f)s,k. Considerando sólo las cadenas finitas en K(f) y K(F)k se obtienen los respectivos grupos de homología seccional con soportes compactos de f. el homomorfismo natural de la homología seccional de f:X→B en la homología singular de B con cadenas localmente finitas Pn:Hn(f)s→HIIn(B) le permitió definir el grado seccional de la función f, denotado deg(f), cuando B es una variedad orientada de dimensión n por la f´romula deg(f) = card (HIIn(B)/Im Pn>-1. En el caso en que X, B y f sean de clase C∞, se puede utilizar el grupo de homología seccional k-veces derivable Hn(f)s,ken lugar de Hn(f)s, y obtener el grado de k-veces derivable de f: degk(f). Estas nociones le permitieron probar que la anulación de deg(f) es necesaria para que f admita una sección continua y, en el caso diferenciable, que degk(f)=O es necesario para que f tenga una sección de clase Ck. Redefiniendo los grupos de homología con soportes compactos de f. Shih obtiene nuevos grados (ver el capítulo VIII de esta Tesis), que coinciden con los anteriores cuando la variedad V es compacta, y demuestra un teorema de caracterización del nuevo grado seccional continuo de f:Y→X, con la condición de que f sea un espacio fibrado localmente trivial cuya base X sea una variedad topológica conexa orientada de dimensión n y cuya fibra sea un CW-complejo finito conexo. Shih no presenta demostraciones ni propiedades de las homologías, ni indica la categoría explícitamente. Lo hace François Lalonde, quien ha dedicado su Tesis a estudiar sistemáticamente la homología seccional con soportes compactos. Ha demostrado que cumple los axiomas de Eilenberg-Steenrod, excepto el de escisión, en una categoría adecuada y que los grupos correspondientes no son invariantes de homotopía continua. Esto último es un inconveniente para el cálculo, pero es fundamental para poder aplicar esta teoría a los problemas de ecuaciones en derivadas parciales o integrales pues estos problemas no son invariantes por homotopía. La These d’Etat de Lalonde está dedicada a calcular la homología seccional diferenciable de clase CKde las funciones diferenciables f:X2→X1que localmente son de la forma RnxRm→Rn. estas funciones, que se llaman k-submersiones, engloban a los fibrados localmente triviales y a las submersiones en el sentido ordinario. El resultado que obtiene, para lo cual introduce nuevas teorías de homología que llama homología de p-campos transversos y homología de “plongements”, es el siguiente: TEOREMA S. Sea f:X2→X1 una k0-submersión (2≤k0≤∞). Cualquiera que sea 1≤k≤k0, el morfismo inyectivo P2:C(f)k→c(Xz) del grupo de cadenas seccionales finitas de clase Ck de f en el grupo de cadenas singulares finitas del espacio Xz, dado por la proyección (Δq,σ,γ)→(Δq,γ), índice un isomorfismos P2*sobre los grupos de homología en las dimensiones inferiores a n = dim Xz y un epimorfismos en dimensión n (los grupos de homología seccional de f son nulos en las dimensiones >n). Aquí vamos a presentar una teoría de homología más simple que las anteriores, que es una teoría de Eilenberg-Steenrod (es decir, que cumple escisión) y que la definición de grado coincide con las anteriores. El método adoptado consiste en construir una apropiada teoría de bordismo tomando como modelos las seudovariedades. Los ciclos geométricos asociados a una función continua f:Y→X son cuaternas (P, σ, γ, P) donde P es una seudovariedad, σ y γ son funciones continuas tales que σ=f•γ y P es un recubrimiento por subpoliedros compactos de P, de forma que σ es “casi inyectiva” en cada subpoliedro PiЄP. Decimos que una función σ:Pi→X definida en un poliedro Pi es “casi inyectiva” si existe un poliedro Q, un p.l. –epimorfismo π:Pi→Q y una función continua inyectiva υ:Q→X tales que σ = υ•π. El usar funciones “casi inyectivas” es para que sea posible la construcción “cilindro de un ciclo” que permite hacer bordante un ciclo a sí mismo (como se sabe, esto es esencial en toda teoría de bordismo). En nuestro caso el cilindro del ciclo (P, σ, γ; P) es (PxI, σ•pr1, γ•pr1; PxI), donde I es el intervalo cerrado [0.1], pr1 es la proyección canónica sobre el primer factor yPxI = {PixI | PiЄP}; es evidente que σ•pr1 no puede ser inyectiva, ni siquiera “inyectiva a trozos”. Una posible desventaja de este procedimiento de representar los ciclos seccionales frente a otros procedimientos que se imaginen, es que estamos obligados a estudiar si las funciones σ son o no inyectivas en cada PiЄP. La solución que tenemos es que en cada clase de seudobordismo hay al menos un ciclo (P, σ, γ;P) en el cual σ es inyectiva en cada PiЄP. Una característica positiva del bordismo aquí presentado es que hay una equivalencia natural con la homología de un apropiado complejo de cadenas que llamamos homología seccional casi-inyectiva, lo cual nos permite compararlo directamente con la homología singular y demostrar que el grado definido con nuestra homología coincide con el Shih. También se da el seudobordismo seccional diferenciable de clase Ck. Su estudio se basa en un caso particular, el seudobordismo de casi-inmersiones difeomorfas de clase Ck, de forma análoga a lo que ocurre con la homología seccional diferenciables y la homología de “plongements”, pero sin necesitar nada parecido a la homología de p-campos transversos, lo cual, junto al uso de las técnicas de aproximación de inmersiones difeormorfas diferenciales, produce una teoría mucho más sencilla que la dada por Lalonde. Los ciclos seccionales diferenciables de clase Ck (P, σ, γ; P)kasociados a una función f:Y→X de clase Ck son ciclos seccionales con funciones σ y γ continuas que cumplen ciertas condiciones de diferenciabilidad respecto a las variedades cX = X U∂x∂X*[0,1) y cY = Y U∂Y∂Y*[0,1), que se obtienen pegando a X y a Y sendos collares diferenciables. La razón de esto es haber observado que los simplices (Δn, σ, γ)k de la homología seccional diferencial de Shih son, por definición, tales que σ se prolonga a una inmersión difeomorfa s:U→X siendo U un entorno abierto de Δn en el espacio euclideo generado por Δn. por lo tanto, si dim X = n resulta que σΔn∩∂x = 0 γ, en consecuencia ninguna de las cadenas de dimensión igual a la de X que se forme con éstos símplices puede tener como borde una cadena cuyo soporte en X esté enteramente sobre ∂x, con lo cual no tiene sentido tratar con dicha homología seccional el problema de extender una sección definida en ∂x a todo X, ni tampoco tiene sentido tratar con ellas el problema de Dirichlet para una ecuación diferencial. Con dicha teoría de homología, los resultados que presentamos y consideramos más sobresalientes son: (1) Se da un tratamiento unificado de una teoría del grado de Shih utilizando, tanto en el caso compacto como en el no compacto, una teoría de bordimos seccional que es una teoría de homología ordinaria, en el sentido de Eilenberg-Steenrod, que permite un tratamiento más simple que en el realizado por Lalonde. (2) Demostrar que dichos grados nos permite: 2a) Caracterizar la variedades triangulables; 2b) Caracterizar la existencia de secciones de funciones continuas y de funciones diferenciables. Por otro lado, sobresale el haber extendido el “Teorema S” de LALONDE al caso de homología con soportes propios. Hay que observar que los cálculos con éstas homologías son difíciles, los cuales corresponde a la dificultad de los problemas que pretende tratar. Este trabajo, por tanto, no pretende más que sentar las bases de un nuevo método para el futuro estudio de dichos problemas. La memoria se presenta organizada en dos partes, cada una de las cuales consta a su vez de varios capítulos. La primera parte está dedicada a la homología seccional de funciones continuas y al grado continuo. En la segunda parte se trata el caso diferenciable, con especial énfasis en los fibrados localmente triviales y las submersiones. La extensión de algunos capítulos es reducida porque, para facilitar la lectura, se han suprimido las demostraciones que se pudieran obtener con fáciles pero laboriosas adaptaciones de demostraciones anteriores, y porque se ha querido facilitar la localización de los resultados, renunciado por ello a refundirlos con otros. A lo largo de esta memoria, y también en esta introducción, las referencias bibliográficas aparecen entre corchetes, mientras que las referencias internas a las definiciones, notas y resultados de este trabajo se hace colocando entre paréntesis las dos cifras con las cuales están ordenados lexicográficamente, la primera de las cuales india el capítulo en que está situado y la segunda el lugar dentro de él. Así, la cita “(2.4)” se refiere al ítem cuarto del capítulo segundo.
  • Acceso AbiertoTesis Doctoral
    Hacia una concepción generalizada de la abducción, su modelización en lógicas no clásicas y su implementación en herramientas informáticas
    (2016-07-15) Sarrión Morillo, Enrique; Nepomuceno Fernández, Ángel; Soler Toscano, Fernando; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial; Universidad de Sevilla. HUM609: Grupo de Logica, Lenguaje e Informacion
    Comenzamos esbozando de modo informal una propuesta muy general del concepto de abducción, señalando cuáles son los caracteres esenciales de este tipo de inferencia y qué otros rasgos que tradicionalmente se le han impuesto deben ser eliminados. A continuación, ya desde una perspectiva puramente lógica, y partiendo de una modelización formal muy próxima a la que hemos considerado como versión canónica de la abducción ordinaria, hemos presentado en un nivel metalingüístico (no vinculado a ningún sistema lógico concreto) diversas propuestas que, además de liberar este concepto de sus dependencias de las lógicas clásicas, lo generalizan de distintas maneras –por ejemplo, contemplando la posibilidad de que el problema abductivo o/y la solución sean todo un conjunto de fórmulas, o también incorporando la posibilidad de que se establezcan condiciones adicionales a las que ya debe cumplir la versi ón inicial (a la que hemos etiquetado como plana)–. A partir de la citada posibilidad que admite nuevas condiciones, y que constituye lo que hemos denominado como abducción ordinaria cualificada, hemos elaborado los conceptos de abducción ordinaria cualificada preferencial y abducción ordinaria cualificada preferencial estratégica. Además, en todo este proceso de generalización y diversificación se han incorporado componentes que no se recogen en las formalizaciones que encontramos en la literatura lógica consultada e igualmente se han hecho distinciones novedosas respecto de algunos elementos que sí han sido considerados con anterioridad. Todo ello ha permitido que se pueda expandir considerablemente la tipología de inferencias que aparecen en los estudios sobre esta materia. En el caso de la abducción sistémica también hemos acometido esa doble tarea de sacar a la luz ciertas componentes que no habían sido previamente contempladas y de elaborar una versión que, partiendo de la que aquí es considerada como canónica, permita aplicarla en muchas otras situaciones que no reúnen los requisitos que tácitamente se recogen en las escasas publicaciones que hasta la fecha han abordado esta cuestión. Extendemos a ella algunas de las distinciones que ya fueron consideradas en relación con la abducción ordinaria y, de este modo, reforzamos los argumentos que defienden la naturaleza esencialmente abductiva de este tipo de inferencia. Similar proceso hemos seguido y similares logros hemos alcanzado en el caso de la novedosa abducción holística, la cual presentamos como una manera de unificar y superar a los dos grandes modos que ya hemos señalado: ordinario y sistémico. Creemos que un estudio profundo de una relación inferencial debe afrontar su nivel puramente estructural, aunque somos conscientes que en el mismo no queda todo determinado y en cualquier caso hay que completarlo con otros estudios en los que ya se ha agregado información acerca del lenguaje o de la semántica concreta del sistema lógico. Nuestro estudio estructural, que se aparta en algunas exigencias de los más comunes en la literatura, fijó inicialmente la mirada en las relaciones inferenciales binarias y dentro de ellas, de manera especial, en la deducción clásica y en una más novedosa que aquí denominamos deducción plural. Ambas, junto a la también novedosa relación de deducción cualificada, son estudiadas por nosotros con un fin puramente instrumental. Para cada uno de los tipos de relaciones inferenciales binarias que hemos distinguido se ha presentado un buen número de propiedades y hemos indagado cuáles se derivan de otras consideradas básicas. En el caso de las relaciones inferenciales ternarias, dado que son nuestro objetivo, el estudio tipológico es más detallado si cabe. En todos los casos hemos indicado qué restricciones se tienen que imponer y qué propiedades se satisfacen en cada uno de los tipos. El haberlo hecho paso a paso, ‘aislando’ cada uno de los requisitos elementales que se pueden agregar al caso base (que es una relación inferencial que coincide con la que Atocha Aliseda denomina inferencia abductiva), nos permite tener intuiciones sobre otros tipos aquí no abordamos explícitamente pero que se pueden construir mediante la adecuada combinación de los citados caracteres básicos. Del mismo modo, hemos probado de manera rigurosa importantes resultados (llamados teoremas de representación) sobre la caracterización estructural de ciertos tipos de relaciones inferenciales abductivas, dando con ello respuesta a problemas que han permanecido abiertos casi dos décadas. Finalmente hemos presentado varias aportaciones que o bien facilitan la modelización de ciertos tipos de inferencia abductiva en sistemas lógicos pertenecientes al ámbito de la Lógica Epistémica Dinámica (entendida en sentido amplio) o bien mejoran varias de sus propiedades con el objetivo de posibilitar su implementación en herramientas informáticas. En concreto nuestro tratamiento lógico de la acción de olvidar se muestra como un buen candidato para la modelización de la abducción ante anomalía en el ámbito citado.
  • Acceso AbiertoPremio Extraordinario de Doctorado USTesis Doctoral
    Un entorno para la experimentación virtual con modelos computacionales basados en sistemas P
    (2015-02-02) Valencia Cabrera, Luis; Pérez Jiménez, Mario de Jesús; Riscos Núñez, Agustín; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial; Universidad de Sevilla. TIC193: Computacion Natural
    ** Introducción Desde el principio de los tiempos, el Hombre se ha visto abocado a resolver problemas. En un principio problemas muy concretos, como huir de un peligro inminente, buscar un alimento en un momento dado o resguardarse del frío para continuar ejerciendo sus funciones vitales hasta nuevo aviso. Pero para avanzar en ello, es necesario plantear posibles estrategias que ayuden a resolver los problemas de manera general, no para cada caso particular, y para ello es conveniente dotarse de las mejores herramientas posibles. Para solucionar toda esa clase de problemas, la evolución ha llevado a la Humanidad a acumular una base de teorías y experiencias, de reflexiones y vivencias, que le ha ido proporcionando cada vez un mayor conocimiento de los fenómenos, de los entornos y circunstancias, de los problemas a los que se enfrenta, de sus herramientas y de sus posibles soluciones. No todos los problemas son de la misma naturaleza ni se pueden atacar de la misma forma. Algunos de ellos pueden ser resueltos de forma mecánica; es decir, mediante un procedimiento sistemático que no requiera un conocimiento mayor del problema a resolver sino, más bien, unas habilidades para ejecutar unas tareas elementales. En ese sentido, cualquier entidad o máquina, viva o no, que sea capaz de llevar a cabo cada tarea o instrucción recogida en el procedimiento sistemático, será capaz de ejecutar la solución del problema resuelto de forma mecánica. Un avance muy sustancial en la resolución de problemas de este tipo, resolubles de manera mecánica, se produjo con la aparición de los ordenadores electrónicos en la década de los cuarenta del pasado siglo, sobre las bases sentadas un siglo antes por parte de Charles Babbage y Augusta Ada Lovelace, cuando la tecnología del momento aún no estaba preparada para materializar el diseño realizado a nivel conceptual. Este salto cuantitativo que supuso la irrupción de los ordenadores electrónicos, tuvo un impacto enorme en el siglo XX y continúa hasta nuestros días. Se espera que esta tendencia continúe, si bien desde 1983 sabemos gracias a un resultado de R. Churchhouse que la velocidad de los procesadores electrónicos tiene un tope que jamás podrán superar. Esa limitación se traduce en la imposibilidad práctica de resolver problemas muy relevantes en la vida real mediante ordenadores con soporte electrónico. Por ello se procede a la búsqueda de caminos alternativos en una huida hacia delante, vías novedosas denominadas no convencionales. Una posibilidad por la que el Hombre ha optado en numerosas ocasiones es la de mirar a la Naturaleza como fuente de inspiración. La observación de que muchos de los fenómenos que tienen lugar en la Naturaleza pueden ser interpretados como procedimientos de cálculo, es la base de la Computación Natural, disciplina científica que recoge diversos paradigmas computacionales cuyo diseño se ha inspirado en procesos procedentes de la Naturaleza. En los últimos años, desde su creación por parte de Gheorghe Paun en 1998, la Computación Celular con Membranas ha sido uno de los paradigmas de la Computación Natural que más ha atraído a la la comunidad científica, proporcionando un marco computacional inspirado en la estructura y el funcionamiento de las células vivas, que tiene presente la capacidad de las células para efectuar de manera simultánea un gran número de procesos a nivel bioquímico, a nivel de cada compartimento de cada célula, de cada célula de un tejido, etc. En este sentido, ha habido diversas iniciativas desde su creación, tomando como referencia la célula y su estructura jerárquica interna, los tejidos formados por células o finalmente la comunicación que se produce entre neuronas, para producir modelos de computación muy diversos con un "tronco común". Esos nuevos modelos tratan de dar respuestas satisfactorias a la resolución de problemas que afectan al ser humano, concretamente la resolución de problemas abstractos mediante métodos mecánicos, pero tratando de salvar las limitaciones inherentes a la tecnología electrónica. La computación celular con membranas proporciona modelos de computación orientado a máquinas, descritos a través de la sintaxis de los dispositivos o máquinas cuya ejecución (de acuerdo con una semántica muy singular) proporciona, teóricamente, todas las funciones computables del modelo. En definitiva, resolver un problema dentro de estos modelos de computación conllevará la descripción de las máquinas correspondientes. Los dispositivos teóricos (las máquinas) de la computación celular con membranas se denominan, genéricamente, sistemas P. En función de la idea que los haya inspirado, tendremos sistemas P que trabajan a modo de células, sistemas P que trabajan a modo de tejidos o, incluso, sistemas P que trabajan a modo de neuronas. A su vez, existen diversas variantes de estos sistemas, la mayor parte de las cuáles se han demostrado universales (en el sentido de tener la misma potencia computacional que las máquinas de Turing), por lo que, de acuerdo con la tesis de Church-Turing serán capaces de resolver, teóricamente, cualquier problema resoluble mecánicamente (en la acepción informal del término). Además, se ha demostrado que muchas de esas máquinas tienen la capacidad de resolver de manera eficiente (en el sentido de la semántica paralela, maximal y no determinista) problemas computacionalmente duros; en particular, problemas NP{completos. Obviamente, la resolución en tiempo polinomial de esos problemas en tiempo polinomial no implica una demostración negativa de la conjetura P =/= NP ya que la solución polinomial se obtiene a cambio de usar una cantidad exponencial de espacio. De esta forma se ha producido un avance interesante en la resolución de problemas complejos en un modelo de computación que reduce drásticamente el número de pasos necesarios para responder a instancias del problema. No obstante, surge la problemática de implementar esos nuevos modelos de computación bioinspirados en máquinas cuyo soporte no sea el electrónico, a fin de sacar rentabilidad a las soluciones teóricas propuestas. ¿Disponemos de la tecnología necesaria para materializar ese diseño en una máquina real? La respuesta es que, de momento, no es posible. Precisamente esto es lo que sucedió, por ejemplo, a mediados del siglo XIX con las ideas de Babagge cuya máquina analítica establecía elementos básicos muy similares a los que rigen el funcionamiento de los ordenadores actuales. Desgraciadamente el sueño de Babbage nunca pudo ser hecho realidad debido, principalmente, a que la tecnología de la época no estaba lo "suficientemente preparada" para la ocasión. La aparición de nuevos paradigmas teóricos de computación abre muchas expectativas, si bien debe venir acompañado de importantes avances tecnológicos que permitan hacer realidad la construcción de máquinas inspiradas en esos paradigmas computacionalmente potentes. Dicho lo cual y a pesar de que esos nuevos modelos están aún bastante lejos de poder ser implementados, obviamente en soporte no electrónico, la tarea de diseño de máquinas teóricas debe continuar, a la vez que habrá que esforzarse en construir simuladores que permitan su fácil manejo, aunque no capture de manera literal la semántica de esos modelos. Si bien esos simuladores no podrán explotar toda la eficiencia computacional de las soluciones diseñadas, sí servirán, en cambio, para explorar las capacidades de los modelos, sus limitaciones, su expresividad y potencia descriptiva, así como profundizar en la solución de los problemas empleando el tipo de procedimientos mecánicos asociados a estos novedosos modelos. Desde la aparición de la Computación Celular con Membranas, se han proporcionado un buen número de soluciones a problemas tanto en el ámbito de lo que podríamos denominar problemas de la vida real, más cercanos a necesidades claramente identificables por las personas "de a pie", como a problemas aparentemente un poco más lejanos que tienen una alta complejidad pero que, a su vez, pueden representar (modelizar) a problemas concretos interesantes. Ese es el caso, por ejemplo, del problema de la 3-coloración de un grafo, aparentemente "un problema matemático" teórico pero subyacente a muchos problemas de la vida real en cuya esencia se pueda encontrar una serie de elementos que deben satisfacer restricciones que involucran a varios de ellos como, por ejemplo la construcción de determinados tipos de circuitos o la elaboración de un calendario de exámenes, entre otros. En el caso particular de fenómenos interesantes que aparecen en la vida real, es importante tratar de profundizar en el conocimiento en un sentido más amplio. Para ello, hay que capturar los detalles considerados como más relevantes acerca de los fenómenos que se estudian, a través de un proceso de abstracción en el que se determinen los elementos fundamentales a considerar (los fenómenos de la vida real en toda su extensión involucran, generalmente, demasiadas variables, parámetros y circunstancias, muchas de ellas desconocidas para nosotros) y se desechen otros que son considerados menos importantes para el fenómeno objeto de estudio. Como resultado de este proceso, analizando una serie de aspectos de un buen número de elementos y las posibles interrelaciones entre los mismos, se obtienen modelos formales que tratan de reproducir lo más fielmente posible la realidad del fenómeno que se estudia. Las soluciones a este tipo de problemas reales y de alta complejidad proporcionadas en el marco de un modelo de computación, deben venir acompañadas del desarrollo de simuladores a medida para resolver de forma práctica instancias concretas de los mismos que son las que suelen aparecer en la vida cotidiana. Estos simuladores ad hoc son asistentes del diseñador de soluciones para materializar respuestas concretas a problemas concretos que son modelizados por el problema abstracto. Es decir, parafraseando aquello de que "pan para hoy, hambre para mañana" es importante concentrar el esfuerzo en la resolución de problemas complejos abstractos de tal manera que las soluciones para instancias concretas tengan un amplio alcance. En este contexto, un paso fundamental en la búsqueda de esa solución lo más general posible de los problemas en el ámbito de la simulación de sistemas celulares fue el marcado por P-Lingua. Esta plataforma software proporciona un lenguaje estándar para la especificación de estos dispositivos computacionales, junto con herramientas para el reconocimiento y depuración del lenguaje, así como simuladores capaces de reproducir la dinámica que tendría el sistema real si su materialización ya fuera una realidad. De este modo, en su búsqueda por solucionar problemas y tras la evidencia de las limitaciones encontradas en otros paradigmas, el hombre no sólo cuenta con una sólida teoría y una experiencia en el ámbito de la computación celular con membranas, sino que también dispone de unas herramientas para la simulación de los diseños realizados, a falta de una implementación real. El diseñador de modelos formales en computación celular con membranas puede, así, dedicar sus esfuerzos al diseño de soluciones en el estudio de los fenómenos, sin preocuparse del desarrollo de simuladores para cada problema particular, dada la disponibilidad de simuladores de propósito general capaces de hacer ese trabajo. Así pues, partamos de que ya se dispone de un lenguaje, unas herramientas y unos simuladores de los sistemas P para analizar su dinámica a partir de un escenario (configuración) inicial hasta una determinada situación de parada. A pesar de todo ello, siempre existirá una gran cantidad de problemas a los que nos podremos enfrentar y todo esfuerzo será pequeño con la inmensidad que nos queda por conocer, más y mejor, el mundo que nos rodea y resolver los problemas derivados de ello. Ahora bien, ¿qué limitaciones encontramos y dónde podría aportarse un valor a la hora de resolver problemas? Como se ha comentado, se han proporcionado herramientas para evitar el desarrollo de simuladores a medida, se ha resuelto ese problema general y, por tanto, ya podemos centrarnos en diseñar los sistemas P para resolver los problemas y éstos podrán ser ejecutados mediante los simuladores proporcionados, pero... La provisión de un modelo computacional que resuelva un problema relacionado, por ejemplo, con un ecosistema real por parte del diseñador de sistemas P, ¿puede ayudar por sí solo a la mejor toma de decisiones por parte del ecólogo experto? ¿la existencia de un sistema P que represente, de forma sorprendentemente ajustada, una ruta señalizadora de proteínas relacionada con la apoptosis (muerte celular programada) puede dotar por sí sola de una herramienta interesante para el biólogo molecular? La respuesta no puede ser un categórico no, pero si leemos el enunciado de la pregunta podremos estar de acuerdo en que antes de convertirse en herramienta útil este sistema debe ser bien comprendido por el ecólogo o el biólogo molecular, o bien, si estamos en el ámbito de los problemas NP-completos, por el lógico, el matemático o el experto en el dominio del problema del que se trate. Con independencia del campo de aplicación o del dominio del problema relevante a resolver, si se va a trabajar con variantes de modelos de computación celular con membranas, el experto en el dominio del que se trate deberá tener ciertas nociones de los sistemas P. Para cada situación que se plantee el experto, en su profundización en el problema concreto en el que esté trabajando, deberá volver al modelo con el fin de codificar en el lenguaje P-Lingua, los datos correspondientes a la situación e interpretar la evolución de los elementos que participan en el modelo, en términos de la dinámica del sistema real que trata de analizar y cuyos problemas desea de resolver. De esta manera, el diseñador de modelos en computación celular, ha conseguido resolver un problema con carácter general, dotar de un marco computacional que resuelve el problema abstracto e, incluso, codificarlo en P-Lingua, trabajar con el reconocedor del lenguaje, depurarlo y "reproducirlo" con el simulador de propósito general a disposición en el ámbito de los sistemas P. Este es el nivel al que trabaja el diseñador de sistemas P, con un profundo conocimiento de este tipo de variantes, y capaz de interactuar con los expertos del dominio del problema profundizando en ese conocimiento sobre los fenómenos, así como con los sistemas y simuladores. Sin embargo, aparecen una serie de dificultades cuando hay que emplear este modelo con el fin de que sea una herramienta útil para la mejora en el conocimiento y la gestión práctica de los fenómenos por parte de los expertos en el dominio del problema. Sin olvidar que tales expertos deben trabajar con las mismas herramientas del diseñador, situarse al mismo nivel de abstracción y afrontar distintos problemas con esas herramientas. El principal objetivo del trabajo presentado en esta tesis es dar un nuevo paso en la senda abierta por P-Lingua para la resolución de problemas mediante modelos no convencionales, más específicamente, mediante modelos de computación celular con membranas. Se trata, pues, de acercar tales herramientas a los expertos en los fenómenos, procesos o sistemas complejos objetos de estudio, de tal modo que se acorte el salto importante que va desde el modelo teórico o la solución a nivel de diseñador, hasta la disposición de una solución práctica a nivel del usuario final. En este punto nos podemos preguntar si existen modelos de computación celular con membranas que hayan sido utilizados en la resolución de problemas reales por los expertos en los dominios en cuestión, ajenos a las interioridades de los sistemas P. En efecto, eso se ha logrado para determinadas variantes pero, tradicionalmente, eso ha supuesto un coste muy significativo, en ocasiones teniendo que desarrollar simuladores software a medida para resolver un problema concreto y, en otras ocasiones, pese a disponer de simuladores y diseños generales basados en P-Lingua se ha tenido que desarrollar una aplicación software de alto nivel para situarlo en el dominio del usuario final. El entorno de simulación presentado se denomina MeCoSim (Membrane Computing Simulator) y pretende cubrir esa necesidad, resolver ese problema. Es decir, se trata de implementar un mecanismo general para poner a disposición de los usuarios aplicaciones adaptables a cada problema particular, abstrayéndoles de las interioridades de los sistemas P y los modelos basados en ellos, que utilizarán como herramienta, a modo y manera que P-Lingua proporciona a los diseñadores de sistemas P herramientas que los abstraigan del detalle de los reconocedores y simuladores. De esta forma, se pretende que esos problemas reales a los que se ha buscado una vía alternativa de solución, una especie de huida hacia delante para resolverlos, sobreponiéndonos a las limitaciones de paradigmas convencionales, pasen del ámbito de los diseñadores de sistemas P a terminar constituyéndose en herramientas útiles para la resolución práctica de instancias tratables de los problemas, precisamente para aquellos que estén especialmente interesados en aumentar su conocimiento acerca de los fenómenos, pudiendo así erigirse en potentes asistentes para la mejor toma de decisiones acerca de la gestión de los fenómenos de interés. Para acometer el objetivo anterior y poner un pequeño granito de arena, una lágrima en el mar del conocimiento para sumar a los esfuerzos de tantos hermanos en la búsqueda de resolver los problemas que atañen a la Humanidad, se ha desarrollado el trabajo que, en la medida de lo posible, se trata de plasmar en los contenidos que se estructuran a continuación. ** Contenido de la memoria La memoria de esta tesis se ha estructurado en tres partes principales que en conjunto constituyen ocho capítulos cuyos contenidos pasan a describirse a continuación. Parte I: Preliminares La primera parte de la memoria se organiza a través de una serie de capítulos preliminares que tratan de sentar las bases sobre las que se sustenta el cuerpo de la tesis. El Capítulo 1 parte de la necesidad del Hombre de resolver problemas relevantes para su vida, y la existencia de determinadas soluciones a los mismos a través de procedimientos mecánicos. A continuación, se observa las limitaciones de los dispositivos de propósito general (ordenadores) que tienen soporte electrónico, a la hora de resolver determinadas instancias de problemas relevantes, así como la necesidad de explorar vías alternativas. Para ello, se recurre a métodos computacionales no convencionales inspirados en la Naturaleza viva, dentro de la disciplina de la Computación Natural. A continuación se profundiza un poco en el paradigma de la Computación Celular con Membranas, inspirada en la estructura y el funcionamiento de las células de los organismos vivos. Se proporcionan definiciones detalladas de varios dispositivos computacionales enmarcados en este paradigma, a saber, los sistemas P de transición, los sistemas P con membranas activas, así como los sistemas P que trabajan a modo de tejidos (incluyendo reglas de división celular o de separación celular). Además, se introduce el concepto de resolubilidad en tiempo polinomial de un problema de decisión en el ámbito de estos sistemas celulares. La última parte del capítulo está dedicada a explicar el rol que cumplen los simuladores de sistemas P, las características que debe presentar una buena plataforma de simulación y, finalmente, se realiza una revisión general de los simuladores paralelos desarrollados hasta el momento para sistemas P. El Capítulo 2 aborda la problemática que se encuentra el investigador a la hora de estudiar sistemas dinámicos complejos, con especial atención a aquellos que se dan en el mundo real y son de interés. Se profundiza en el proceso de modelización de la porción del mundo real que es objeto de estudio, desde la abstracción de los aspectos más relevantes de los fenómenos en cuestión, pasando por la representación de los elementos involucrados en los mismos, hasta el uso y finalidad de los modelos diseñados para aumentar el conocimiento acerca de los fenómenos estudiados. Además, se analiza la posibilidad de emplear los modelos como herramientas útiles para ayudar a una toma de decisiones más informada por parte de los gestores de los fenómenos de interés. Seguidamente se define con precisión el concepto de modelo formal y las fases que caracterizan el proceso de modelización, se recuerda la noción de modelo de computación y se describen las propiedades deseables en todo buen modelo formal. A continuación, se analizan diversas aproximaciones de modelos formales, tanto computacionales como no computacionales, y el tema finaliza describiendo la aleatoriedad inherente a los procesos que se dan en la vida real, así como la idoneidad de capturar ciertos aspectos de la misma a través de modelos matemáticos, estocásticos o probabilísticos. El Capítulo 3 centra la atención en el ámbito de los modelos computacionales dentro del paradigma de la Computación Celular con Membranas, fundamentalmente en su empleo como marco de modelización para el estudio de fenómenos de interés de la vida real. Así, se da un marco formal uniforme, los sistemas P multientorno, para la representación de sistemas complejos de diversa índole, bajo los que se encuentran dos aproximaciones diferentes que encajan perfectamente dentro del marco: los sistemas P multicompartimentales, para fenómenos moleculares y celulares de naturaleza esencialmente estocástica, y los sistemas P de dinámica de poblaciones, una aproximación probabilística empleada, fundamentalmente, en procesos relacionados con la evolución en el tiempo de ecosistemas reales. El resto del capítulo presenta una serie de algoritmos que permiten capturar la semántica de los dos tipos de sistemas multientorno mencionados, planteando además distintas posibilidades a la hora de reproducir la dinámica de los sistemas, en función de las características de los fenómenos bajo estudio, como la existencia de cooperación entre individuos o la competencia por determinados recursos. Parte II: Cuerpo El cuerpo de esta memoria presenta el núcleo del trabajo realizado, describiendo en primer lugar las herramientas conceptuales, metodológicas y prácticas desarrolladas y, a continuación, la aplicación a diversos problemas de interés, tanto para la resolución de problemas de la vida real como problemas teóricos computacionalmente duros, como son los problemas NP-completos. El Capítulo 4 se centra en la descripción del entorno de simulación MeCoSim, software de propósito general para la validación experimental y experimentación virtual de los modelos analizados en los capítulos anteriores. Inicialmente se introducen las herramientas, su origen y los objetivos principales que motivan su aparición. A continuación, se detalla la estructura interna del entorno y las principales funcionalidades proporcionadas tanto al diseñador de sistemas P, poniendo a su disposición un conjunto de facilidades para el diseño, depuración e introspección del modelo, como al usuario final, al que se le proporciona una aplicación visual que le permite trabajar a alto nivel centrando su atención en el estudio de los fenómenos de su interés, introduciendo sus escenarios y realizando las simulaciones correspondientes hasta obtener resultados, abstrayéndole de los detalles internos de los modelos. El capítulo finaliza con la presentación de una metodología para la solución de problemas en el ámbito de los sistemas P, desde el estudio inicial de los fenómenos hasta la utilización de herramientas adaptadas a las necesidades del usuario, para la experimentación virtual y la posible toma de decisiones anticipando las posibles consecuencias de los potenciales escenarios estudiados. El Capítulo 5 se enfoca en la novedosa aparición de los simple kernel P systems, una variante de sistemas celulares que pretende actuar como modelo integrador, aglutinador de diferentes elementos de diversas variantes de sistemas P que ya habían sido diseñadas y utilizadas con anterioridad. El objetivo de esa variante consiste en proporcionar un único formalismo capaz de simular la acción de la mayor cantidad de variantes de sistemas P anteriores. De esta manera, será posible realizar determinados tratamientos y estudios sobre los modelos, como la verificación de propiedades sobre los mismos, de manera uniforme, sin necesidad de desarrollar dichos mecanismos para cada variante de sistemas P. Además, los elementos introducidos en este modelo formal tratan de facilitar el diseño de soluciones basadas en sistemas P, en lugar de muchos otros formalismos destinados a disponer de un conjunto mínimo de elementos capaz de resolver el mayor espectro posible de problemas con dichos ingredientes. Los capítulos 6 y 7 presentan sendas aplicaciones en el ámbito de los problemas de la vida real y de los problemas NP-completos. El Capítulo 6 comienza ofreciendo una panorámica y un poco de historia sobre la simulación de modelos de sistemas dinámicos que se dan en la vida real, e ilustra el uso del entorno y la metodología desarrollados en el Capítulo 4 para la modelización, análisis y simulación de fenómenos interesantes que aparecen en la vida real; por ejemplo, la gestión de un ecosistema acuático afectado por la presencia de una especie exótica invasora. Este caso de estudio supone un gran reto dado que se trata de un sistema complejo con un gran número de procesos y elementos involucrados interrelacionados entre sí y, a la vez, permite mostrar las capacidades proporcionadas por las herramientas anteriores. Finalmente, en este capítulo se detalla la aplicación de P-Lingua y MeCoSim como entorno vertebrador de la metodología propuesta, articulando las diversas fases de la misma. El Capítulo 7 se centra en el uso de la plataforma proporcionada para trabajar en la resolución de problemas NP-completos bien conocidos. Para ello, se parte de la representación de dichos problemas y su modelización mediante sistemas P, incluyendo su traducción a P-Lingua, su reconocimiento sintáctico, depuración y simulación e introspección del sistema paso a paso. Así se consigue proveer una aplicación visual de alto nivel basada en MeCoSim para la introducción de diversas entradas adaptadas para cada problema, de tal manera que sea reconocible por el usuario y se pueda trabajar en el problema obviando las interioridades de su solución, con el fin de obtener resultados visuales adecuados para el dominio de su problema. Parte III: Resultados La tercera parte de la memoria pone el punto (y seguido) a la labor desempeñada. El Capítulo 8 comienza con las conclusiones extraídas del trabajo realizado y de las aportaciones comentadas en esta sección. Posteriormente se proponen las principales líneas de investigación en las que ya se ha empezado a trabajar para continuar la senda abierta por esta tesis, así como las principales ideas de líneas de trabajo futuro que se considera podrían aportar grandes avances en la búsqueda de soluciones prácticas a problemas relevantes en diversos ámbitos. Finalmente, se presentan algunos apéndices adicionales que tratan de cumplir varios objetivos complementarios al núcleo del trabajo presentado. Por un lado, intentar hacer justicia con la cantidad de paquetes software de los que se ha hecho uso durante el desarrollo del trabajo, ilustrando la funcionalidad que han aportado al entorno de simulación. Por otro lado, presentar el sitio web desarrollado para ilustrar las funcionalidades de MeCoSim a través de páginas, documentos y vídeos de uso, con el fin de servir de repositorio de aplicaciones, modelos y escenarios para las soluciones basadas en sistemas P. El objetivo es facilitar a la comunidad de Membrane Computing el trabajo práctico de modelización y simulación con sistemas P, así como la provisión a los usuarios de aplicaciones adaptadas a cada problema real para los usuarios finales, a modo y manera que las herramientas anteriores han sido de gran utilidad para el desarrollo del entorno de simulación MeCoSim. ** Aportaciones Entre las aportaciones realizadas a lo largo del desarrollo del presente trabajo, queremos destacar las que se relacionan a continuación. - Diseño de una metodología para el empleo de soluciones basadas en sistemas P como herramientas capaces de asistir en la búsqueda de mayor conocimiento y la gestión de los problemas de interés, involucrando los pasos necesarios desde el estudio inicial del problema hasta la disposición de la aplicación software adaptada al mismo, así como los procesos de modelización, depuración, introspección, parametrización y personalización de aplicaciones, simulación, visualización, análisis de datos, extracción de propiedades invariantes y verificación de las mismas. - Desarrollo de un entorno de simulación capaz de proporcionar los mecanismos adecuados para dar respuesta a los objetivos planteados por la metodología anterior, tanto a los diseñadores de soluciones basadas en sistemas P como a los usuarios finales de las aplicaciones. Estos mecanismos desarrollados han debido proporcionar el entorno de simulación general, y herramientas que sean a la vez lo suficientemente generales y flexibles para que puedan tratar cualquier solución basada en sistemas P, como personalizables para poder adaptarse a las necesidades de los usuarios de la mayor diversidad posible de problemas. - Diseño e implementación de un mecanismo de extensibilidad para poder dotar al entorno general de nuevos mecanismos de extensibilidad, que amplíen la funcionalidad general, tanto actual como prevista del entorno, a través de una arquitectura de plugins en la que poder incorporar programas basados tanto en tecnologías similares a las empleadas por MeCoSim como completamente externos, conectables a MeCoSim a partir de una simple configuración. De tal modo que podamos llamar a dichos programas externos desde nuestro entorno general a través del sistema operativo. Los mecanismos desarrollados van en la línea de uno de los principales objetivos de MeCoSim: la vertebración, estandarización y articulación del proceso de modelización y simulación aunando para ello cuantos más herramientas y esfuerzos mejor, haciendo bueno el principio holístico de que el todo es mayor que la suma de las partes, premisa con la que ya se presentara MeCoSim en el congreso BIC-TA 2010 en la República Popular China. - Desarrollo e integración de plugins para la solución de requisitos específicos en respuesta a diversos problemas, como la introducción de fórmulas proposicionales de forma amigable para el usuario (SAT plugin), la visualización de grafos para problemas relacionados con este tipo de elementos (Graphs plugin), la extracción de invariantes mediante la conexión con el software Daikon (Daikon plugin), la simulación externa a través del software Spin (Promela plugin), o el proyecto piloto para el desarrollo de funcionalidades adicionales para MeCoSim codificadas en diversos lenguajes de programación (con una conexión inicial al compilador GHC tras introducir código Haskell) (Languages Integration plugin). - Diseño de un lenguaje para simple kernel P systems en P-Lingua, capturando los elementos esenciales del marco y extendiendo P-Lingua para incorporar los elementos necesarios. - Desarrollo de herramientas para el reconocimiento léxico-sintáctico y desarrollo de un simulador en el framework de P-Lingua, con el fin de reconocer, depurar y simular soluciones basadas en simple kernel P systems. - Aplicación de la metodología y las herramientas desarrolladas a un buen número de problemas de la vida real (aves carroñeras, rebeco, alianzas de plantas, tritones, anfibios, peces, mejillón cebra, pandemias, redes genéticas y producción animal porcina) y a un conjunto de problemas NP-completos (SAT, 3-COL, Subset Sum, Partition, Vertex Cover y Broadcasting). - Desarrollo de un sitio web para la descarga e instalación de MeCoSim y difusión de la información documental y audiovisual para el empleo de las funcionalidades básicas proporcionadas, así como para la centralización de repositorios de aplicaciones, modelos y escenarios correspondientes a soluciones basadas en sistemas P. ** Conclusiones El trabajo que se ha desarrollado en la presente memoria trata de dar un paso hacia la disposición real, para el común de los seres humanos, de herramientas prácticas con las que resolver problemas en el ámbito citado. Para ello, se ha diseñado una metodología que va desde la observación del problema a resolver, hasta la provisión de una aplicación software para asistir en la profundización del conocimiento acerca de los fenómenos objetos de estudio, a través de la realización de experimentos virtuales que permita anticipar la respuesta del sistema estudiado antes diferentes posibles escenarios que pudieran ser de interés. Junto con la metodología referida, se ha desarrollado un entorno virtual de simulación, MeCoSim (Membrane Computing Simulator), que articula la propuesta metodológica a través de herramientas lo suficientemente generales y flexibles para abarcar el mayor número de problemas posible y, a la vez, lo suficientemente personalizables con el fin de ajustarse a las necesidades de cada aplicación particular de la metodología. Este entorno permite la liberación de aplicaciones adaptadas para los usuarios finales de cada problema particular, dotándole internamente de todas las herramientas proporcionadas por el marco de P-Lingua, pero de forma transparente, de tal manera que los sistemas P no sean para él el fin sino el medio. Por ello, para los diseñadores de sistemas P el entorno actuará como un IDE (Integrated Development Environment) suponiendo una capa adicional de introspección y tratamiento visual de los modelos basados en sistemas P, mientras que para los usuarios finales se dispondrá de una aplicación visual para la gestión del fenómeno de su interés, adaptado al dominio del problema. En esa aplicación se podrán introducir los datos específicos del escenario a estudiar, realizar los experimentos virtuales simulando el comportamiento del sistema real y observar las salidas derivadas del modelo, mediante datos tabulados o gráficas que ilustren la evolución de las componentes básicas, en el ámbito de estudio del usuario final, ajeno a las interioridades de los sistemas P subyacentes y la complejidad del marco sobre el que se construye. Los objetivos de este entorno requieren que sea, además, lo suficientemente extensible para permitir la ampliación de la cobertura de problemas y funcionalidades actuales y previstas. Para ello, se ha desarrollado, junto con el entorno de simulación MeCoSim, una arquitectura de plugins que permita la integración con otras herramientas software implementadas en la misma o en tecnologías distintas a la empleada por MeCoSim. El entorno se ha integrado con algunas herramientas externas a través del desarrollo de un primer conjunto de plugins, como es el caso del detector de invariantes Daikon o el Model Checker Spin. Además, se han desarrollado otros plugins para la visualización de estructuras basadas en grafos, con el fin de incorporar desde MeCoSim funciones en otros lenguajes de programación, como Haskell, o bien para la introducción de fórmulas proposicionales en un lenguaje muy similar al empleado por los lógicos. Conviene destacar la colaboración realizada en el desarrollo y adaptación de distintos simuladores en el ámbito de los sistemas P de Dinámica de Poblaciones, de los sistemas P de tejido, o de los sistemas P que funcionan a modo de nueronas. Ante la diversidad de estos sistemas y variantes, para determinados fines, como es el caso de la verificación automática de modelos, se ha participado en el diseño y aplicación práctica de un nuevo formalismo con la finalidad de unificar, homogeneizar en cierto sentido, la variedad existente de sistemas P. Dentro de éstos, se ha desarrollado en el marco de P-Lingua tanto el lenguaje como un reconocedor léxico-sintáctico, así como un primer simulador de un subconjunto de los mismos: los simple kernel P systems. El diseño de una metodología y el desarrollo de una serie de herramientas vertebradoras no pueden, por sí solo, demostrar la utilidad de una propuesta para la resolución práctica de problemas reales que afecten al ser humano, tanto en el ámbito de aplicaciones sobre la vida real como en la resolución de problemas NP-completos bien conocidos que puedan repercutir, en última instancia, sobre otros problemas más cercanos a las necesidades del día a día. Afortunadamente, desde sus inicios, este desarrollo ha venido acompañado de múltiples aplicaciones prácticas de la metodología y de las herramientas, a un gran número de problemas tanto de la vida real (estudio de la dinámica de ecosistemas reales como el quebrantahuesos en la zona pirenaico catalana o en el pirineo navarro, análisis de los efectos de los pestivirus en la población del rebeco en el pirineo catalán, reintroducción de una especie de pájaros en una zona de Cataluña, alianzas de plantas, tritones, desarrollo y crecimiento de anfibios en estanques naturales, producción animal porcina, plan de control de la especie invasora del mejillón cebra, estudio de pandemias o redes de genes, etc.) como del ámbito de la teoría de la complejidad computacional, aplicándose a la resolución de problemas NP-completos bien conocidos como SAT, 3-COL, Subset Sum, Vertex Cover o Partition. En ellas se han hecho uso de diversas variantes como los sistemas P con membranas activas, sistemas P de tejidos con reglas de división o de separación celular, sistemas P que trabajan a modo de neuronas, simple kernel P systems o sistemas P de Dinámica de Poblaciones (PDP systems) en el ámbito de la modelización de sistemas complejos. Las herramientas desarrolladas están siendo utilizadas en la actualidad por grupos de investigación de diversas universidades en Lleida, Sheffield (U.K.), Bucarest y Pitesti (Rumanía), Wuhan y Chengdu (China). Además, tenemos conocimiento de la aparición de nuevos trabajos que comienzan a emplearlas (el último de ellos, que tengamos constancia, desde Malasia).
  • Acceso AbiertoTesis Doctoral
    Verificación formal en ACL2 del Algoritmo de Buchberger
    (2003-12-18) Medina Bulo, Inmaculada; Alonso Jiménez, José Antonio; Ruiz-Reina, José-Luis; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    En este trabajo se han desarrollado los elementos necesarios para especificar, implementar y verificar la correción del algoritmo de Buchberger para el cálculo de bases de Gröbner, utilizando para ello un sistema de razonamiento automatizado (ACL2); esto incluye la formalización completa y precisa de toda la teoría matemática subyacente. Concretamente: -El desarrollo de una teoría computacional sobre los anillos de polinomios de múltiples variables. -La obtención de un orden natural a los polinomios de múltiples variables y demostración de su buena fundamentación. -La representación de los conceptos asociados a los ideales polinómicos de manera que sea posible razonar sobre ellos de manera automatizada. -El desarrollo de una teoría computacional sobre las reducciones polinómicas estableciendo su relación con las reduccines abstractas. -La representación de los conceptos asociados a las bases de Gröbner de manera que sea posible razonar sobre ellos de manera automatizada. -La implementación del algoritmo de Buchberger, especificar sus propiedades y demostrar su corrección. -La obtención de un procedimiento de decisión verificado para el problema de la pertenencia al ideal. Como se observa, nuestro énfasis se sitúa en la automatización del razonamiento. Dentro de los sistemas de razonamiento adecuados para este tipo de tareas hemos elegido a ACL2. Este sistema merece especial atención, ya que formaliza un subconjunto de COMMON LISP, un lenguaje de programación real. De hecho, LISP y sus dialectos se han usado tradicionalmente en la escritura de sistemas de Álgebra Computaciones. Por otro lado, ACL2 es especialmente bueno razonando por inducción. En este sentido, estamos ante un demostrados heurístico que incorpora no sólo potentes procedimientos de decisión, sino también estrategias sobre cómo abordar diferentes tipos de pruebas, cuándo expandir la definición de una función o generalizar un término, etc. La mayor parte de las ideas presentes en ACL2 provienen de un sistema anterior, NQTHM, también llamado el demostrador de teoremas de Boyer y Moore. ACL2 comienza a ser desarrollado en 1989 por Boyer, Moore y Kaufmann como una mejora sustancias de NQTHM, estando las últimas versiones desarrolladas fundamentalmente por los dos últimos autores. Hemos demostrado todos los teoremas (del orden de un millar) que aparecen durante la consecución de los objetivos mencionados en este sistema. Desde el punto de vista lógico, ACL2 es una lógica de primer orden con igualdad sin cuantificadores ni tipos y con funciones recursivas totales. La lógica incluye dos principios de extensión importantes, definición y encapsulado, y un principio de inducción que permite razonar sobre las funciones definidas por recursión. Como se observa, la lógica en sí es muy débil; en particular, la ausencia de cuantificadores supone una restricción importante de la lógica de primer orden. El hecho de que las funciones hayan de ser totales y la ausencia de tipos también tienen su impacto en la expresividad. Éste es el precio que hay que pagar por una mayor automatización: generalmente, nos concentramos en escribir las proposiciones y lemas intermedios que permiten al sistema demostrar un teorema complejo, proporcionándole de vez en cuando indicaciones cuando se desvía de nuestro plan preconcebido. Discutamos brevemente la importancia del algoritmo de Buchberger como justificación de su elección para nuestro trabajo. El gran desarrollo sufrido en la última década por el Álgebra Computacional ha dado como resultado la proliferación de numerosos sistemas de propósito general como MATHEMATICA. Éstos son la culminación de los resultados teóricos obtenidos en el último medio siglo, uno de cuyos descubrimientos centrales fue debido a B. Buchberger cuando en 1965 proporcionó un algoritmo para construir bases de Gröbner, que se emplean fundamentalmente para resolver el problema de la pertenencia en ideales polinómicos. h. Hironaka ya había demostrado poco antes la existencia de este tipo de bases, a las que llamó bases estándar, pero su demostración no era constructiva y no arrojaba ninguna luz sobre el problema de cómo calcularlas. El algoritmo de Buchberger, aunque al principio no tuvo demasiada difusión, causó finalmente un gran impacto en áreas muy diversas. Originalmente, se empleó para resolver problemas en Geometría Algebraica, pero ha sido aplicado con éxito en campos tan diversos como la Teoría de la Codificación, Estadística, Investigación Operativa y Teoría de Invariantes. También se ha empleado para automatizar el razonamiento en lógicas modales. Hoy día está implementado en la mayoría de los sistemas como MUPAD, MAPLE y MATHEMATICA, por citar sólo algunos. También existen unos pocos sistemas especialmente diseñados para proporcionar implementaciones particularmente eficientes del algoritmo de Buchberger como COCOA, SINGULAR, y MACAULAY. Es por esto que consideramos que disponer de implementaciones verificadas del algoritmo de Buchberger es importante. No obstante, esta tarea no resulta sencilla y lo primero que puede sorprendernos es la riqueza de estructuras algebraicas subyacentes a la propia definición del algoritmo de Buchberger y el esfuerzo que hay que dedicar a su formalización. Hay que emplear un cuerpo conmutativo de coeficientes para definir los monomios con los que construir polinomios de múltiples variables, los monomios deben poseer un orden admisible con el que inducir otro sobre los polinomios. Luego, hay que construir funciones de reducción apropiadas entre los polinomios. Para asegurar la corrección del algoritmo y proporcionar un procedimiento de decisión verificado para el problema de la pertenencia al ideal aumenta la variedad de estructuras implicadas y el esfuerzo necesario. En primer lugar, hay que definir el concepto de ideal polinómico finitamente generado y su congruencia inducida. Por otro lado, las funciones de reducción conviene estudiarlas en el marco, más general, de las relaciones de reducción abstractas. Sólo entonces, podemos obtener los resultados necesarios sobre las bases de Gröbner. Es en este esfuerzo adicional donde radica la diferencia entre programar el algoritmo y demostrar que es correcto.
  • Acceso AbiertoTesis Doctoral
    Developing effcient simulators for cell machines
    (2016-02-02) Macías Ramos, Luis Felipe; Pérez Jiménez, Mario de Jesús; Valencia Cabrera, Luis; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    Membrane Computing, introduced by Gh. Paun at the end of 1998, is a relatively young branch of Natural Computing providing non-deterministic distributed parallel computing models whose computational devices are called membrane systems or P systems. These systems are inspired by some basic biological features, specifically by the structure and functioning of the living cells, as well as from the way the cells are organized in tissues, organs, and organisms. There are basically three ways to categorize membrane systems: cell-like P systems, tissue-like P systems, and neural-like P systems, also called Spiking Neural P systems (SN P systems, for short). Cell-like P systems arrange a series of membranes in a hierarchical way, inspired by the inner structure of the biological cells. Tissue-like P systems arrange elemental membranes in nodes of a directed graph, inspired from the cell inter-communication in tissues. Similarly, Spiking Neural P systems also arrange elemental membranes in nodes of a directed graph, while taking inspiration from the way in which neurons exchange information by the transmission of electrical impulses (spikes) along axons. In general, P systems operate by applying rewriting rules de_ned over multisets of objects associated to the di_erent membranes, in a synchronized non-deterministic maximally parallel way. P systems show a double level of parallelism: a first level comprises parallel application of rules within individual membranes, while a second level comprises all the membranes working simultaneously, that is, in parallel. These features make P systems powerful computing devices. In particular, the double level of parallelism allows a space-time tradeoff enabling the generation of an exponential workspace in polynomial time. As such P systems are suitable to tackle relevant real-life problems, usually involving NP-complete problems. Moreover, P systems are excellent tools to investigate on the computational complexity boundaries, in particular tackling the P versus NP problem. In this way, by studying how the ingredients relative to their syntax and semantics a_ect to their ability to e_ciently solve NP-complete problems, sharper frontiers between e_ciency and non-efficiency can be discovered. Despite of their attractive properties, working with P systems immediately drives to an important inconvenient: due to constraints of current technology, P systems are yet to be fully implemented in vivo, in vitro, or even in silico, because of their massively parallel, distributed, and non-deterministic nature. Thus, practical computations of P systems are driven by silicon- based simulators, and hence their potential results are compromised by the physical limitations of silicon architectures. They are often inefficient or not suitable when dealing with some P system features, such as the exponential workspace creation, non-determinism and massive parallelism. Consequently, developing e_cient simulation tools for P systems becomes an indispensable task in order to both assist in the computational complexity study involving such systems, as well as in the development and verification of solutions to relevant real-life problems. The main contributions derived from the work object of this dissertation are the following: -Finding sharper computational complexity boundaries by modelling solutions to NP-complete problems in terms of cell-like P systems in CDC and CSC. -Developing a simulation tools for membrane systems in CDC and CSC within the P-Lingua framework. These tools have played a major role as assistants in the speci_cation and formal verification of the aforementioned solutions. -Defining new SN P systems variants and the corresponding simulation tools, within the P-Lingua framework. Also, simulation support for a wide range of existing SN P systems variants has been included into that framework. -Defining efficient simulation tools for Fuzzy Reasoning SN P systems working on High Performance Computation platforms, namely CUDA- enabled devices.
  • Acceso AbiertoTesis Doctoral
    Semilinear order property and infinite games
    (2016-01-22) Simões Loureiro, Manuel José; Cordón Franco, Andrés; Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
    En este trabajo se analiza la determinación de juegos de Lipschitz y Wadge, junto con la propiedad de ordenación semilineal, estrechamente relacionada con estos juegos, en el contexto de la Aritmética de segundo orden y el programa de la Matemática inversa (Reverse Mathematics). En primer lugar, se obtienen pruebas directas, formalizables en la Aritmética de segundo orden, de la determinación de los juegos de Lipschitz y Wadge para los primeros niveles de la Jerarquía de diferencias de Hausdorff. A continuación, se determinan los axiomas de existencia suficientes para la formalización de dichas pruebas dentro de los subsistemas clásicos de la Aritmética de segundo orden (fórmula). Finalmente, en algunos casos se muestra que dichos axiomas de existencia son óptimos, probando que resultan ser equivalentes (sobre un subsistema débil adecuado, como RCA0 o ACA0) a las correspondientes formalizaciones de los principios de determinación o de ordenación semilineal. Los principales resultados obtenidos son los siguientes: Teorema A. Sobre RCA0 son equivalentes: (fórmula) (el principio de determinación para juegos de Lipschitz entre subconjuntos del espacio de Cantor que son diferencia de dos cerrados). (fórmula) (la propiedad de ordenación semilineal de la reducibilidadLipschitz entre subconjuntos del espacio de Cantor que son diferencia de dos cerrados). Teorema B. Sobre RCA0 son equivalentes: (fórmula) (el principio de determinación para juegos de Lipschitz entre subconjuntos abiertos o cerrados del espacio de Baire). Teorema C. Sobre ACA0 son equivalentes: (fórmula) (el principio de determinación para juegos de Lipschitz entre subconjuntos del espacio de Baire que son simultáneamente abiertos y cerrados). (fórmula) (la propiedad de ordenación semilineal de la reducibilidadLipschitzentre subconjuntos del espacio de Baire simultáneamente abiertos y cerrados).