An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction

23 p. -- An extended abstract of this work appears in the proceedings of the 2012 ACM/IEEE Symposium on Logic in Computer Science

The Role of the Demand for Environmental Quality in Driving Transitions to Low-Polluting Energy Sources

4 p.

Sistema de control y supervisión para una instalación industrial basado en técnicas de computación en la nube.

[ES]Hasta ahora, el control y monitorización de una instalación industrial se realiza desde la sala de control situada en las propias instalaciones de la planta. Cada unidad de control guarda y envía los datos a un ordenador que después se envían a uno central, siguiendo un orden jerárquico, en el que se visualizan ante un operario. Hoy en día, sin embargo, con el auge de los dispositivos móviles inteligentes, se puede conseguir que esa supervisión de la planta industrial se pueda hacer desde cualquier lugar. Podemos visualizar esos datos de control en nuestra mano y mandar órdenes a cada unidad desde nuestro teléfono inteligente. Esto es lo que se ha conseguido hacer con este proyecto, en el que se ha modelizado una instalación industrial basada en una cadena de montaje con tres unidades.

Caracterización del retardo en redes definidas por software para monitorizar el nivel de utilización de recursos.

[ES]Este proyecto busca caracterizar el retardo sufrido por los mensajes de estadísticas en las redes definidas por software cuando la red se encuentra en estado de saturación. Para ello, se utilizarán los paquetes OpenFlow que utiliza el controlador OpenDaylight para comunicarse con los nodos presentes en la red, a través de ellos se podrán monitorizar los recursos consumidos por los servicios instalados. Toda la monitorización se llevará a cabo desde el controlador, el módulo de monitorización optimizado en este proyecto permitirá al controlador conocer el valor promedio del ancho de banda consumido en instantes de tiempo de hasta un segundo en todos los nodos de la red donde se hayan instalado los servicios. Estos valores podrán ser utilizados para controlar el ancho de banda consumido por los distintos servicios dentro de una red, realizando acciones desde el propio controlador sobre aquellos servicios que superen el límite establecido.

Beyond Q-Resolution and Prenex Form: a Proof System for Quantified Constraint Satisfaction

We consider the quanti fied constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quanti fication, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.