Termination and cost analysis: Complexity and precision issues

The research in this thesis is related to static cost and termination analysis. Cost analysis aims at estimating the amount of resources that a given program consumes during the execution, and termination analysis aims at proving that the execution of a given program will eventually terminate. These analyses are strongly related, indeed cost analysis techniques heavily rely on techniques developed for termination analysis. Precision, scalability, and applicability are essential in static analysis in general. Precision is related to the quality of the inferred results, scalability to the size of programs that can be analyzed, and applicability to the class of programs that can be handled by the analysis (independently from precision and scalability issues). This thesis addresses these aspects in the context of cost and termination analysis, from both practical and theoretical perspectives. For cost analysis, we concentrate on the problem of solving cost relations (a form of recurrence relations) into closed-form upper and lower bounds, which is the heart of most modern cost analyzers, and also where most of the precision and applicability limitations can be found. We develop tools, and their underlying theoretical foundations, for solving cost relations that overcome the limitations of existing approaches, and demonstrate superiority in both precision and applicability. A unique feature of our techniques is the ability to smoothly handle both lower and upper bounds, by reversing the corresponding notions in the underlying theory. For termination analysis, we study the hardness of the problem of deciding termination for a speci�c form of simple loops that arise in the context of cost analysis. This study gives a better understanding of the (theoretical) limits of scalability and applicability for both termination and cost analysis.

Highly efficient potentiometric glucose biosensor based on functionalized InN quantum dots

We present a fast, highly sensitive, and efficient potentiometric glucose biosensor based on functionalized InN quantum-dots (QDs). The InN QDs are grown by molecular beam epitaxy. The InN QDs are bio-chemically functionalized through physical adsorption of glucose oxidase (GOD). GOD enzyme-coated InN QDs based biosensor exhibits excellent linear glucose concentration dependent electrochemical response against an Ag/AgCl reference electrode over a wide logarithmic glucose concentration range (1 × 10−5 M to 1 × 10−2 M) with a high sensitivity of 80 mV/decade. It exhibits a fast response time of less than 2 s with good stability and reusability and shows negligible response to common interferents such as ascorbic acid and uric acid. The fabricated biosensor has full potential to be an attractive candidate for blood sugar concentration detection in clinical diagnoses.

Reachability-based acyclicity analysis by Abstract Interpretation

In programming languages with dynamic use of memory, such as Java, knowing that a reference variable x points to an acyclic data structure is valuable for the analysis of termination and resource usage (e.g., execution time or memory consumption). For instance, this information guarantees that the depth of the data structure to which x points is greater than the depth of the data structure pointed to by x.f for any field f of x. This, in turn, allows bounding the number of iterations of a loop which traverses the structure by its depth, which is essential in order to prove the termination or infer the resource usage of the loop. The present paper provides an Abstract-Interpretation-based formalization of a static analysis for inferring acyclicity, which works on the reduced product of two abstract domains: reachability, which models the property that the location pointed to by a variable w can be reached by dereferencing another variable v (in this case, v is said to reach w); and cyclicity, modeling the property that v can point to a cyclic data structure. The analysis is proven to be sound and optimal with respect to the chosen abstraction.

Embedding logical frameworks in scala

El Framework Lógico de Edimburgo ha demostrado ser una poderosa herramienta en el estudio formal de sistemas deductivos, como por ejemplo lenguajes de programación. Sin embargo su principal implementación, el sistema Twelf, carece de expresividad, obligando al programador a escribir código repetitivo. Este proyecto presenta una manera alternativa de utilizar Twelf: a través de un EDSL (Lenguaje Embebido de Dominio Específico) en Scala que permite representar firmas del Framework Lógico, y apoyándonos en Twelf como backend para la verificación, abrimos la puerta a diversas posibilidades en términos de metaprogramación. El código fuente, así como instrucciones para instalar y configurar, está accesible en https://github.com/akathorn/elfcala. ---ABSTRACT---The Edinburgh Logical Framework has proven to be to be a powerful tool in the formal study of deductive systems, such as programming languages. However, its main implementation, the Twelf system, lacks expressiveness, requiring the programmer to write repetitive code. This project presents an alternative way of using Twelf: by providing a Scala EDSL (Embedded Domain Specific Language) that can encode Logical Framework signatures and relying on Twelf as a backend for the verification, we open the door to different possibilities in terms of metaprogramming. The source code, along with instructions to install and configure, is accessible at https://github.com/akathorn/elfcala

How should the sustainability of the location of dry ports be measured? A proposed methodology using Bayesian networks and multi-criteria decision analysis

The global economic structure, with its decentralized production and the consequent increase in freight traffic all over the world, creates considerable problems and challenges for the freight transport sector. This situation has led shipping to become the most suitable and cheapest way to transport goods. Thus, ports are configured as nodes with critical importance in the logistics supply chain as a link between two transport systems, sea and land. Increase in activity at seaports is producing three undesirable effects: increasing road congestion, lack of open space in port installations and a significant environmental impact on seaports. These adverse effects can be mitigated by moving part of the activity inland. Implementation of dry ports is a possible solution and would also provide an opportunity to strengthen intermodal solutions as part of an integrated and more sustainable transport chain, acting as a link between road and railway networks. In this sense, implementation of dry ports allows the separation of the links of the transport chain, thus facilitating the shortest possible routes for the lowest capacity and most polluting means of transport. Thus, the decision of where to locate a dry port demands a thorough analysis of the whole logistics supply chain, with the objective of transferring the largest volume of goods possible from road to more energy efficient means of transport, like rail or short-sea shipping, that are less harmful to the environment. However, the decision of where to locate a dry port must also ensure the sustainability of the site. Thus, the main goal of this article is to research the variables influencing the sustainability of dry port location and how this sustainability can be evaluated. With this objective, in this paper we present a methodology for assessing the sustainability of locations by the use of Multi-Criteria Decision Analysis (MCDA) and Bayesian Networks (BNs). MCDA is used as a way to establish a scoring, whilst BNs were chosen to eliminate arbitrariness in setting the weightings using a technique that allows us to prioritize each variable according to the relationships established in the set of variables. In order to determine the relationships between all the variables involved in the decision, giving us the importance of each factor and variable, we built a K2 BN algorithm. To obtain the scores of each variable, we used a complete cartography analysed by ArcGIS. Recognising that setting the most appropriate location to place a dry port is a geographical multidisciplinary problem, with significant economic, social and environmental implications, we consider 41 variables (grouped into 17 factors) which respond to this need. As a case of study, the sustainability of all of the 10 existing dry ports in Spain has been evaluated. In this set of logistics platforms, we found that the most important variables for achieving sustainability are those related to environmental protection, so the sustainability of the locations requires a great respect for the natural environment and the urban environment in which they are framed.

Economics of Wheat in Egypt

Este estudio pretende estimar la eficiencia y la productividad de las principales provincias de la producción de trigo en Egipto. Los datos utilizados en este estudio son datos de panel a nivel de provincias del período 1990-2012, obtenidos del Ministerio de Agricultura y Recuperación Tierras, y de la Agencia Central de Movilización Pública y Estadística, Egipto. Se aplica el enfoque de fronteras estocásticas para medir la eficiencia (función de producción de Cobb-Douglas) y se emplean las especificaciones de Battese y Coelli (1992) y (1995). También se utiliza el índice de Malmquist como una aproximación no paramétrica (Análisis de Envolvente de Datos) para descomponer la productividad total de los factores de las principales provincias productoras de trigo en Egipto en cambio técnico y cambio de eficiencia. El coeficiente de tierra es positivo y significativo en los dos especificaciones Battese y Coelli (1992) y (1995), lo que implica que aumentar la tierra para este cultivo aumentaría significativamente la producción de trigo. El coeficiente de trabajo es positivo y significativo en la especificación de Battese y Coelli (1992), mientras que es positivo y no significativo en la especificación de Battese y Coelli (1995). El coeficiente de la maquinaria es negativo y no significativo en las dos especificaciones de Battese y Coelli (1992) y (1995). El coeficiente de cambio técnico es positivo y no significativo en la especificación de Battese y Coelli (1992), mientras que es positiva y significativo en la especificación de Battese y Coelli (1995). Las variables de efectos del modelo de ineficiencia Battese y Coelli (1995) indican que no existe impacto de las diferentes provincias en la producción de trigo en Egipto; la ineficiencia técnica de la producción de trigo tendió a disminuir durante el período de estudio; y no hay ningún impacto de género en la producción de trigo en Egipto. Los niveles de eficiencia técnica varían entre las diferentes provincias para las especificaciones de Battese y Coelli (1992) y (1995); el nivel mínimo medio de eficiencia técnica es 91.61% en la provincia de Fayoum, mientras que el nivel máximo medio de la eficiencia técnica es 98.69% en la provincia de Dakahlia. La eficiencia técnica toma un valor medio de 95.37%, lo que implica poco potencial para mejorar la eficiencia de uso de recursos en la producción de trigo. La TFPCH de la producción de trigo en Egipto durante el período 1990-2012 tiene un valor menor que uno y muestra un declive. Esta disminución es debida más al componente de cambio técnico que al componente de cambio de eficiencia. La disminución de TFPCH mejora con el tiempo. La provincia de Menoufia tiene la menor disminución en TFPCH, 6.5%, mientras que dos provincias, Sharkia y Dakahlia, son las que más disminuyen en TFPCH, 13.1%, en cada uno de ellas. Menos disminución en TFPCH ocurre en el período 2009-2010, 0.3%, mientras que más disminución se produce en TFPCH en el período 1990-1991, 38.9%. La disminución de la PTF de la producción de trigo en Egipto se atribuye principalmente a la mala aplicación de la tecnología. ABSTRACT The objectives of this study are to estimate the efficiency and productivity of the main governorates of wheat production in Egypt. The data used in this study is a panel data at the governorates level, it represents the time period 1990-2012 and taken from the Ministry of Agriculture and Land Reclamation, and the Central Agency for Public Mobilization and Statistics, Egypt. We apply the stochastic frontier approach for efficiency measurement (Cobb-Douglas production function) and the specifications of Battese and Coelli (1992) and (1995) are employed. Also we use Malmquist TFP index as a non-parametric approach (DEA) to decompose total factor productivity of the main governorates of wheat production in Egypt into technical change and efficiency change. The coefficient of land is positive and significant at Battese and Coelli (1992) and (1995) specifications, implying that increasing the wheat area could significantly enhance the production of wheat. The coefficient of labor is positive and significant at Battese and Coelli (1992) specification, while it is positive and insignificant at Battese and Coelli (1995) specification. The coefficient of machinery is negative and insignificant at the specifications of Battese and Coelli (1992) and (1995). The technical change coefficient is positive and insignificant at Battese and Coelli (1992) specification, while it is positive and significant at Battese and Coelli (1995) specification. The variables of the inefficiency effect model indicate that there is no impact from the location of the different governorates on wheat production in Egypt, the technical inefficiency of wheat production tended to decrease through the period of study, and there is no impact from the gender on wheat production in Egypt. The levels of technical efficiency vary among the different governorates for the specifications of Battese and Coelli (1992) and (1995); the minimum mean level of technical efficiency is 91.61% at Fayoum governorate, while the maximum mean level of technical efficiency is 98.69% at Dakahlia governorate. The technical efficiency takes an average value of 95.37%, this implying that little potential exists to improve resource use efficiency in wheat production. The TFPCH of wheat production in Egypt during the time period 1990-2012 has a value less than one and shows a decline; this decline is due mainly to the technical change component than the efficiency change component. The decline in TFPCH is generally improves over time. Menoufia governorate has the least declining in TFPCH by 6.5%, while two governorates, Sharkia and Dakahlia have the most declining in TFPCH by 13.1% for each of them. The least declining in TFPCH occurred at the period 2009- 2010 by 0.3%, while the most declining in TFPCH occurred at the period 1990-1991 by 38.9%. The declining in TFP of wheat production in Egypt is attributed mainly to poor application of technology.

Metodología para la evaluación de la calidad de la localización de puertos secos

La estructura económica mundial, con centros de producción y consumo descentralizados y el consiguiente aumento en el tráfico de mercancías en todo el mundo, crea considerables problemas y desafíos para el sector del transporte de mercancías. Esta situación ha llevado al transporte marítimo a convertirse en el modo más económico y más adecuado para el transporte de mercancías a nivel global. De este modo, los puertos marítimos se configuran como nodos de importancia capital en la cadena de suministro al servir como enlace entre dos sistemas de transporte, el marítimo y el terrestre. El aumento de la actividad en los puertos marítimos produce tres efectos indeseables: el aumento de la congestión vial, la falta de espacio abierto en las instalaciones portuarias y un impacto ambiental significativo en los puertos marítimos. Los puertos secos nacen para favorecer la utilización de cada modo de transporte en los segmentos en que resultan más competitivos y para mitigar estos problemas moviendo parte de la actividad en el interior. Además, gracias a la implantación de puertos secos es posible discretizar cada uno de los eslabones de la cadena de transporte, permitiendo que los modos más contaminantes y con menor capacidad de transporte tengan itinerarios lo más cortos posible, o bien, sean utilizados únicamente para el transporte de mercancías de alto valor añadido. Así, los puertos secos se presentan como una oportunidad para fortalecer las soluciones intermodales como parte de una cadena integrada de transporte sostenible, potenciando el transporte de mercancías por ferrocarril. Sin embargo, su potencial no es aprovechado al no existir una metodología de planificación de la ubicación de uso sencillo y resultados claros para la toma de decisiones a partir de los criterios ingenieriles definidos por los técnicos. La decisión de dónde ubicar un puerto seco exige un análisis exhaustivo de toda la cadena logística, con el objetivo de transferir el mayor volumen de tráfico posible a los modos más eficientes desde el punto de vista energético, que son menos perjudiciales para el medio ambiente. Sin embargo, esta decisión también debe garantizar la sostenibilidad de la propia localización. Esta Tesis Doctoral, pretende sentar las bases teóricas para el desarrollo de una herramienta de Herramienta de Ayuda a la Toma de Decisiones que permita establecer la localización más adecuada para la construcción de puertos secos. Este primer paso es el desarrollo de una metodología de evaluación de la sostenibilidad y la calidad de las localizaciones de los puertos secos actuales mediante el uso de las siguientes técnicas: Metodología DELPHI, Redes Bayesianas, Análisis Multicriterio y Sistemas de Información Geográfica. Reconociendo que la determinación de la ubicación más adecuada para situar diversos tipos de instalaciones es un importante problema geográfico, con significativas repercusiones medioambientales, sociales, económicos, locacionales y de accesibilidad territorial, se considera un conjunto de 40 variables (agrupadas en 17 factores y estos, a su vez, en 4 criterios) que permiten evaluar la sostenibilidad de las localizaciones. El Análisis Multicriterio se utiliza como forma de establecer una puntuación a través de un algoritmo de scoring. Este algoritmo se alimenta a través de: 1) unas calificaciones para cada variable extraídas de información geográfica analizada con ArcGIS (Criteria Assessment Score); 2) los pesos de los factores obtenidos a través de un cuestionario DELPHI, una técnica caracterizada por su capacidad para alcanzar consensos en un grupo de expertos de muy diferentes especialidades: logística, sostenibilidad, impacto ambiental, planificación de transportes y geografía; y 3) los pesos de las variables, para lo que se emplean las Redes Bayesianas lo que supone una importante aportación metodológica al tratarse de una novedosa aplicación de esta técnica. Los pesos se obtienen aprovechando la capacidad de clasificación de las Redes Bayesianas, en concreto de una red diseñada con un algoritmo de tipo greedy denominado K2 que permite priorizar cada variable en función de las relaciones que se establecen en el conjunto de variables. La principal ventaja del empleo de esta técnica es la reducción de la arbitrariedad en la fijación de los pesos de la cual suelen adolecer las técnicas de Análisis Multicriterio. Como caso de estudio, se evalúa la sostenibilidad de los 10 puertos secos existentes en España. Los resultados del cuestionario DELPHI revelan una mayor importancia a la hora de buscar la localización de un Puerto Seco en los aspectos tenidos en cuenta en las teorías clásicas de localización industrial, principalmente económicos y de accesibilidad. Sin embargo, no deben perderse de vista el resto de factores, cuestión que se pone de manifiesto a través del cuestionario, dado que ninguno de los factores tiene un peso tan pequeño como para ser despreciado. Por el contrario, los resultados de la aplicación de Redes Bayesianas, muestran una mayor importancia de las variables medioambientales, por lo que la sostenibilidad de las localizaciones exige un gran respeto por el medio natural y el medio urbano en que se encuadra. Por último, la aplicación práctica refleja que la localización de los puertos secos existentes en España en la actualidad presenta una calidad modesta, que parece responder más a decisiones políticas que a criterios técnicos. Por ello, deben emprenderse políticas encaminadas a generar un modelo logístico colaborativo-competitivo en el que se evalúen los diferentes factores tenidos en cuenta en esta investigación. The global economic structure, with its decentralized production and the consequent increase in freight traffic all over the world, creates considerable problems and challenges for the freight transport sector. This situation has led shipping to become the most suitable and cheapest way to transport goods. Thus, ports are configured as nodes with critical importance in the logistics supply chain as a link between two transport systems, sea and land. Increase in activity at seaports is producing three undesirable effects: increasing road congestion, lack of open space in port installations and a significant environmental impact on seaports. These adverse effects can be mitigated by moving part of the activity inland. Implementation of dry ports is a possible solution and would also provide an opportunity to strengthen intermodal solutions as part of an integrated and more sustainable transport chain, acting as a link between road and railway networks. In this sense, implementation of dry ports allows the separation of the links of the transport chain, thus facilitating the shortest possible routes for the lowest capacity and most polluting means of transport. Thus, the decision of where to locate a dry port demands a thorough analysis of the whole logistics supply chain, with the objective of transferring the largest volume of goods possible from road to more energy efficient means of transport, like rail or short-sea shipping, that are less harmful to the environment. However, the decision of where to locate a dry port must also ensure the sustainability of the site. Thus, the main goal of this dissertation is to research the variables influencing the sustainability of dry port location and how this sustainability can be evaluated. With this objective, in this research we present a methodology for assessing the sustainability of locations by the use of Multi-Criteria Decision Analysis (MCDA) and Bayesian Networks (BNs). MCDA is used as a way to establish a scoring, whilst BNs were chosen to eliminate arbitrariness in setting the weightings using a technique that allows us to prioritize each variable according to the relationships established in the set of variables. In order to determine the relationships between all the variables involved in the decision, giving us the importance of each factor and variable, we built a K2 BN algorithm. To obtain the scores of each variable, we used a complete cartography analysed by ArcGIS. Recognising that setting the most appropriate location to place a dry port is a geographical multidisciplinary problem, with significant economic, social and environmental implications, we consider 41 variables (grouped into 17 factors) which respond to this need. As a case of study, the sustainability of all of the 10 existing dry ports in Spain has been evaluated. In this set of logistics platforms, we found that the most important variables for achieving sustainability are those related to environmental protection, so the sustainability of the locations requires a great respect for the natural environment and the urban environment in which they are framed.