Resumen: We present a new framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. Taking as a starting point previous approaches, the analysis looks for a metering function that under-approximates the number of loop iterations. The key novelty of the framework is the specialization of loops, which is achieved by restricting their enabled transitions to a subset of the inputs combined with the narrowing of their transition scopes. Specialization allows us to find metering functions for complex loops that could not be handled before or be more precise than previous approaches. Technically, it is performed by using quasi-invariants while searching for the metering function, by strengthening the loop guards, and by narrowing the space of non-deterministic choices. We also propose a Max-SMT encoding that takes advantage of the use of soft constraints to force the solver look for more accurate solutions.

En esta ponencia, presentamos DiGeSp-DL 1.0, la primera versión de un modelo neuronal generativo en español. Este modelo ha sido entrenado desde cero usando una arquitectura GPT-2, con el objetivo de enseñarle a realizar la tarea de generar diálogos completos donde podremos condicionar mediante su input una parte de su estructura y contenido. En concreto, podremos indicarle al modelo cuántos turnos de habla tendrá el diálogo, y pedirle que inserte 2 palabras en el turno que le indiquemos. Este trabajo constó de las siguientes etapas:

1. Recopilar un amplio corpus de textos variados en español.
2. Entrenar desde cero un modelo GPT-2 para la generación de textos en español.
3. Construir un corpus de diálogos en español y agregar al inicio de cada uno la información sobre los turnos de habla y su contenido semántico, siguiendo una estructura definida por nosotros.
4. Re-entrenar el modelo de generación GPT-2 en español (del punto 2) para la tarea específica de generación de diálogos guiados por la información de entrada.
5. Implementar un método de generación por fases utilizando el modelo entrenado para guiar la generación de diálogos en español.

Los vehículos aéreos no tripulados (UAV) y sus sistemas sensoriales han emergido durante las últimas décadas como plataformas de gran utilidad en aplicaciones del mundo real tan variadas como la vigilancia de fronteras, extinción de incendios o misiones de búsqueda y rescate. La simulación de este tipo de misiones mediante el modelado de cada uno de los elementos que intervienen, constituye una práctica común con el fin de obtener una mejor comprensión del problema, un mejor desempeño de los objetivos de la misión o la reducción de costes. Centrándonos en las misiones de búsqueda de tiempo mínimo (Minimum Time Search, MTS), donde es necesario encontrar lo antes posible a un objetivo con una posición y dinámica desconocidas, esta tesis tiene como objetivo proporcionar una herramienta multi-plataforma, flexibley eficiente; capaz de formalizar, esquematizar y funcionar como integrador de los múltiples modelos y soluciones alternativas que existen hoy en día para este problema. Haciendo uso de los principios que rigen la ingeniería de sistemas basada en el uso modelos (Model-Based System Engineering, MBSE) junto con el formalismo matemático para la Especificación de Sistemas de Eventos Discretos (Discrete Event System Specification, DEVS), presentamos nuestra herramienta y su uso/despliegue en la nube.