TEORIA DE LA PROGRAMACION

Autor: CALATAYUD RAMOS AYMEE.
Año: 2003.
Universidad: POLITÉCNICA DE MADRID [www.upm.es].
Centro de lectura: FACULTAD DE INFORMÁTICA.
Centro de realización: FACULTAD DE INFORMÁTICA.

Resumen: En esta memoria estudiamos problemas geométricos relacionados con la Localización de Servicios. La Localización de Servicios trata de la ubicación de uno o más recursos (radares, almacenes, pozos exploradores de petróleo, etc.) de manera tal que se optimicen ciertos objetivos (servir al mayor número de usuarios posibles, minimizar el coste de transporte, evitar la contaminación de poblaciones cercanas, etc.). La resolución de este tipo de problemas de la vida real da lugar a problemas geométricos muy interesantes. En el planteamiento geométrico de muchos de estos problemas los usuarios potenciales del servicio son representados por puntos mientras que los servicios están representados por la figura geométrica que mejor se adapta al servicio prestado: un anillo para el caso de radares, antenas de radio y televisión, aspesores, etc, una cuña si el servicio que se quiere prestar es de iluminación, por ejemplo. Estas son las figuras geométricas con las que hemos trabajado. En nuestro caso el servicio será sólo uno y el planteamiento formal del problema es como sigue: dado un anillo o una cuña de tamaño fijo y un conjunto de n puntos en el plano, hallar cuál tiene que ser la posición del mismo para que se cubra la mayor cantidad de puntos. Para resolver estos problemas hemos utilizado arreglos de curvas en el plano. Los arreglos son una estructura geométrica bien conocida y estudiada dentro de la Geometría Computacional. Nos hemos centrado en los arreglos de curvas de Jordan no acotadas que se cortan dos a dos en a lo sumo dos puntos, ya que estos fueron los arreglos con los que hemos tenido que tratar para la resolución de los problemas. De entre las diferentes técnicas para la construcción de arreglos, hemos estudiado el método incremental, ya que conduce a algoritmos más sencillos desde el punto de vista de la codificación. Como resultado de este estudio hemos obtenido nuevas cotas que mejoran la complejidad del tiempo de construcción de estos arreglos con algoritmos incrementales. La nueva cota O(nlambda3(n)) supone una mejora respecto a la cota conocida hasta el momento: O(nlambda4(n)). También hemos visto que en ciertas condiciones estos arreglos pueden construirse en tiempo O(nlambda2(n)), que es la cota óptima para la construcción de estos arreglos. Restringiendo el estudio a curvas específicas, hemos obtenido que los arreglos de n circunferencias de k radios diferentes pueden construirse en tiempo O(n2 min (log(K), alfa (n))), resultado válido también para arreglos de elipses, parábolas o hipérbolas de tamaños diferentes cuando las figuras son todas isotéticas.

Autor: PALOMINO TARJUELO MIGUEL.
Año: 2004.
Universidad: COMPLUTENSE DE MADRID [www.ucm.es].
Centro de lectura: FACULTAD DE CIENCIAS MATEMÁTICAS.
Centro de realización: FACULTAD DE CIENCIAS MATEMÁTICAS.

Resumen: La lógica de reescritura es una extensión de la lógica ecuacional habitual que fue introducida como un modelo parala especificación de sistemas concurrentes que unifica numerosas propuestas anteriores. Desde entonces esta lógica ha demostrado ser un formalismo muy flexible, no solo para la especificación de la concurrencia, sino también como marco lógico y semántico en el que interpretar otras lógicas y modelos de computación. Desde su introducción, se presentó tal lógica como la base de un lenguaje declarativo de especificación y programación, llamado Maude. El estudio de las propiedades matemáticas de la lógica de reescritura es necesario para justificar su uso como herramienta de diseño y especificación. Una de estas propiedades, de fundamental importancia en esta lógica, es la reflexión, que intuitivamente consiste en la habilidad de un sistema computacional o lógico de acceder a su propio metanivel para controlar su comportamiento. En esta tesis damos una demostración detallada de la reflexividad de la lógica de reescritura que extiende trabajos previos sobre versiones más restringidas de la lógica. Además, presentamos un enfoque unificador, aprovechando el trabajo anterior para el estudio de la reflexión en algunas sublógicas de la lógica de reescritura como son la lógica de pertenencia a la lógica de horn con igualdad. La reflexión en la lógica de reescritura tiene, además, una vertiente claramente práctica en la que se propone el uso de la reflexión para metarrozanamiento formal. En esta tesis se avanza en estas ideas, generalizando los principios inductivos propuestos por otro autores y estudiando cómo aplicarlos para demostrar relaciones semánticas entre teorías en la lógica de pertenencia. El otro gran tema de la tesis consiste en la búsqueda de métodos de demostración para la verificación de sistemas que con ella se especifiquen. Para la verificación de propiedades en sistema de reescritura, a partir de su versión 2.0 el sistema Maude incluye un comprobador de modelos. La técnica de comprobación de modelos se ha revelado como una de las historias más felices en el ámbito de la aplicación de métodos formales a la validación de propiedades de sistema a nivel industrial. A pesar de ello, la limitación inherente de los comprobadores de modelos para tratar sistemas infinitos, o simplemente demasiado grandes, ha llevado a muchos investigadores a estudiar técnicas de abstracción con las que superarla. Nuestro interés en este ámbito reside en el estudio de cómo aplicar las técnicas de abstracción en el marco de la lógica de reescritura. Por una parte, nos interesa estudiar posibles generalizaciones de las ideas de abstracción y simulación en un marco categórico más abstracto que en el que habitualmente se presentan. Por otro, cómo definir dichas abstracciones en la lógica de reescritura y Maude. Para ello extendemos la noción habitual de simulación en tres direcciones y mostramos cómo se pueden representar al nivel de la lógica de reescritura mediante generalizaciones sucesivas. También presentamos un estudio de las propiedades básicas de las categorías a que dan lugar dichas simulaciones. Por último, desarrollamos un prototipo en Maude que automatiza el proceso de abstracción, en concreto, el proceso de abstracción de predicadores. Su diseño es reflexivo y hace un uso fundamental del ITP, un demostrador de teoremas desarrollado sobre Madude, al que utiliza como un oráculo capaz de decidir la validez de las numerosas fórmulas en función de las cuales se construye el sistema abstracto.

Autor: Sanchez Penas Juan Jose.
Año: 2006.
Universidad: A CORUÑA [www.udc.es].
Centro de lectura: Facultad de Informática.
Centro de realización: Facultad de Informática.

Resumen: La tesis estudia como ir desde la arquitectura software a la verificación formal de un sistema distribuido. Como motivación y caso de estudio de la investigación, usamos un servidor de video bajo demanda desarrollado por nuestro grupo de investigación. La arquitectura software de dicho sistema es muy flexible y compleja, y mejores herramientas son necesarias para mejorar la calidad del sistema. La tesis estudia como usar métodos formales para eso. Usando diversas herramientas del área, proponemos un método innovador para extraer de forma automática información sobre rendimiento. Como entrada, usamos el código fuente y la configuración del sistema, como salida, información sobre rendimiento y cuellos de botella. Se demuestra el método con el servidor de video y se generaliza para otras herramientas y sistemas.