Modelo para la integración del trazado de infraestructuras lineales en el paisaje y el medio ambiente basado en SIG

El análisis de las diferentes alternativas en la planificación y diseño de corredores y trazados de carreteras debe basarse en la correcta definición de variables territoriales que sirvan como criterios para la toma de decisión y esto requiere un análisis ambiental preliminar de esas variables de calidad. En España, los estudios de viabilidad de nuevas carreteras y autovías están asociados a una fase del proceso de decisión que se corresponde con el denominado Estudio Informativo, el cual establece condicionantes físicos, ambientales, de uso del suelo y culturales que deben ser considerados en las primeras fases de la definición del trazado de un corredor de carretera. Así, la metodología más frecuente es establecer diferentes niveles de capacidad de acogida del territorio en el área de estudio con el fin de resumir las variables territoriales en mapas temáticos y facilitar el proceso de trazado de las alternativas de corredores de carretera. El paisaje es un factor limitante a tener en cuenta en la planificación y diseño de carreteras y, por tanto, deben buscarse trazados más sostenibles en relación con criterios estéticos y ecológicos del mismo. Pero este factor no es frecuentemente analizado en los Estudios Informativos e incluso, si es considerado, los estudios específicos de la calidad del paisaje (estético y ecológico) y de las formas del terreno no incorporan las recomendaciones de las guías de trazado para evitar o reducir los impactos en el paisaje. Además, los mapas de paisaje que se generan en este tipo de estudios no se corresponden con la escala de desarrollo del Estudio Informativo (1:5.000). Otro déficit común en planificación de corredores y trazados de carreteras es que no se tiene en cuenta la conectividad del paisaje durante el proceso de diseño de la carretera para prevenir la afección a los corredores de fauna existentes en el paisaje. Este déficit puede originar un posterior efecto barrera en los movimientos dispersivos de la fauna y la fragmentación de sus hábitats debido a la ocupación parcial o total de las teselas de hábitats con importancia biológica para la fauna (o hábitats focales) y a la interrupción de los corredores de fauna que concentran esos movimientos dispersivos de la fauna entre teselas. El objetivo principal de esta tesis es mejorar el estudio del paisaje para prevenir su afección durante el proceso de trazado de carreteras, facilitar la conservación de los corredores de fauna (o pasillos verdes) y la localización de medidas preventivas y correctoras en términos de selección y cuantificación de factores de idoneidad a fin de reducir los impactos visuales y ecológicos en el paisaje a escala local. Concretamente, la incorporación de valores cuantitativos y bien justificados en el proceso de decisión permite incrementar la transparencia en el proceso de diseño de corredores y trazados de carreteras. Con este fin, se han planteado cuatro preguntas específicas en esta investigación (1) ¿Cómo se seleccionan y evalúan los factores territoriales limitantes para localizar una nueva carretera por los profesionales españoles de planificación del territorio en relación con el paisaje? (2) ¿Cómo pueden ser definidos los corredores de fauna a partir de factores del paisaje que influyen en los movimientos dispersivos de la fauna? (3) ¿Cómo pueden delimitarse y evaluarse los corredores de fauna incluyendo el comportamiento parcialmente errático en los movimientos dispersivos de la fauna y el efecto barrera de los elementos antrópicos a una escala local? (4) ¿Qué y cómo las recomendaciones de diseño de carreteras relacionadas con el paisaje y las formas del terreno pueden ser incluidas en un modelo de Sistemas de Información Geográfica (SIG) para ayudar a los ingenieros civiles durante el proceso de diseño de un trazado de carreteras bajo el punto de vista de la sostenibilidad?. Esta tesis doctoral propone nuevas metodologías que mejoran el análisis visual y ecológico del paisaje utilizando indicadores y modelos SIG para obtener alternativas de trazado que produzcan un menor impacto en el paisaje. Estas metodologías fueron probadas en un paisaje heterogéneo con una alta tasa de densidad de corzo (Capreolus capreolus L.), uno de los grandes mamíferos más atropellados en la red de carreteras españolas, y donde está planificada la construcción de una nueva autovía que atravesará la mitad del área de distribución del corzo. Inicialmente, se han analizado las variables utilizadas en 22 estudios de proyectos de planificación de corredores de carreteras promovidos por el Ministerio de Fomento entre 2006 y 2008. Estas variables se agruparon según condicionantes físicos, ambientales, de usos del suelo y culturales con el fin de comparar los valores asignados de capacidad de acogida del territorio a cada variable en los diferentes estudios revisados. Posteriormente, y como etapa previa de un análisis de conectividad, se construyó un mapa de resistencia de los movimientos dispersivos del corzo en base a la literatura y al juicio de expertos. Usando esta investigación como base, se le asignó un valor de resistencia a cada factor seleccionado para construir la matriz de resistencia, ponderándolo y combinándolo con el resto de factores usando el proceso analítico jerárquico y los operadores de lógica difusa como métodos de análisis multicriterio. Posteriormente, se diseñó una metodología SIG para delimitar claramente la extensión física de los corredores de fauna de acuerdo a un valor umbral de ancho geométrico mínimo, así como la existencia de múltiples potenciales conexiones entre cada par de teselas de hábitats presentes en el paisaje estudiado. Finalmente, se realizó un procesado de datos Light Detection and Ranging (LiDAR) y un modelo SIG para calcular la calidad del paisaje (estético y ecológico), las formas del terreno que presentan características similares para trazar una carretera y la acumulación de vistas de potenciales conductores y observadores de los alrededores de la nueva vía. Las principales contribuciones de esta investigación al conocimiento científico existente en el campo de la evaluación del impacto ambiental en relación al diseño de corredores y trazados de carreteras son cuatro. Primero, el análisis realizado de 22 Estudios Informativos de planificación de carreteras reveló que los métodos aplicados por los profesionales para la evaluación de la capacidad de acogida del territorio no fue suficientemente estandarizada, ya que había una falta de uniformidad en el uso de fuentes cartográficas y en las metodologías de evaluación de la capacidad de acogida del territorio, especialmente en el análisis de la calidad del paisaje estético y ecológico. Segundo, el análisis realizado en esta tesis destaca la importancia de los métodos multicriterio para estructurar, combinar y validar factores que limitan los movimientos dispersivos de la fauna en el análisis de conectividad. Tercero, los modelos SIG desarrollados Generador de alternativas de corredores o Generator of Alternative Corridors (GAC) y Eliminador de Corredores Estrechos o Narrow Corridor Eraser (NCE) pueden ser aplicados sistemáticamente y sobre una base científica en análisis de conectividad como una mejora de las herramientas existentes para la comprensión el paisaje como una red compuesta por nodos y enlaces interconectados. Así, ejecutando los modelos GAC y NCE de forma iterativa, pueden obtenerse corredores alternativos con similar probabilidad de ser utilizados por la fauna y sin que éstos presenten cuellos de botella. Cuarto, el caso de estudio llevado a cabo de prediseño de corredores y trazado de una nueva autovía ha sido novedoso incluyendo una clasificación semisupervisada de las formas del terreno, filtrando una nube de puntos LiDAR e incluyendo la nueva geometría 3D de la carretera en el Modelo Digital de Superficie (MDS). El uso combinado del procesamiento de datos LiDAR y de índices y clasificaciones geomorfológicas puede ayudar a los responsables encargados en la toma de decisiones a evaluar qué alternativas de trazado causan el menor impacto en el paisaje, proporciona una visión global de los juicios de valor más aplicados y, en conclusión, define qué medidas de integración paisajística correctoras deben aplicarse y dónde. ABSTRACT The assessment of different alternatives in road-corridor planning and layout design must be based on a number of well-defined territorial variables that serve as decision-making criteria, and this requires a high-quality preliminary environmental analysis of those quality variables. In Spain, feasibility studies for new roads and motorways are associated to a phase of the decision procedure which corresponds with the one known as the Informative Study, which establishes the physical, environmental, land-use and cultural constraints to be considered in the early stages of defining road corridor layouts. The most common methodology is to establish different levels of Territorial Carrying Capacity (TCC) in the study area in order to summarize the territorial variables on thematic maps and facilitate the tracing process of road-corridor layout alternatives. Landscape is a constraint factor that must be considered in road planning and design, and the most sustainable layouts should be sought based on aesthetic and ecological criteria. However this factor is not often analyzed in Informative Studies and even if it is, baseline studies on landscape quality (aesthetic and ecological) and landforms do not usually include the recommendations of road tracing guides designed to avoid or reduce impacts on the landscape. The resolution of the landscape maps produced in this type of studies does not comply with the recommended road design scale (1:5,000) in the regulations for the Informative Study procedure. Another common shortcoming in road planning is that landscape ecological connectivity is not considered during road design in order to avoid affecting wildlife corridors in the landscape. In the prior road planning stage, this issue could lead to a major barrier effect for fauna dispersal movements and to the fragmentation of their habitat due to the partial or total occupation of habitat patches of biological importance for the fauna (or focal habitats), and the interruption of wildlife corridors that concentrate fauna dispersal movements between patches. The main goal of this dissertation is to improve the study of the landscape and prevent negative effects during the road tracing process, and facilitate the preservation of wildlife corridors (or green ways) and the location of preventive and corrective measures by selecting and quantifying suitability factors to reduce visual and ecological landscape impacts at a local scale. Specifically the incorporation of quantitative and well-supported values in the decision-making process provides increased transparency in the road corridors and layouts design process. Four specific questions were raised in this research: (1) How are territorial constraints selected and evaluated in terms of landscape by Spanish land-planning practitioners before locating a new road? (2) How can wildlife corridors be defined based on the landscape factors influencing the dispersal movements of fauna? (3) How can wildlife corridors be delimited and assessed to include the partially erratic movements of fauna and the barrier effect of the anthropic elements at a local scale? (4) How recommendations of road design related to landscape and landforms can be included in a Geographic Information System (GIS) model to aid civil engineers during the road layout design process and support sustainable development? This doctoral thesis proposes new methodologies that improve the assessment of the visual and ecological landscape character using indicators and GIS models to obtain road layout alternatives with a lower impact on the landscape. These methodologies were tested on a case study of a heterogeneous landscape with a high density of roe deer (Capreolus capreolus L.) –one of the large mammals most commonly hit by vehicles on the Spanish road network– and where a new motorway is planned to pass through the middle of their distribution area. We explored the variables used in 22 road-corridor planning projects sponsored by the Ministry of Public Works between 2006 and 2008. These variables were grouped into physical, environmental, land-use and cultural constraints for the purpose of comparing the TCC values assigned to each variable in the various studies reviewed. As a prior stage in a connectivity analysis, a map of resistance to roe deer dispersal movements was created based on the literature and experts judgment. Using this research as a base, each factor selected to build the matrix was assigned a resistance value and weighted and combined with the rest of the factors using the analytic hierarchy process (AHP) and fuzzy logic operators as multicriteria assessment (MCA) methods. A GIS methodology was designed to clearly delimit the physical area of wildlife corridors according to a geometric threshold width value, and the multiple potential connections between each pair of habitat patches in the landscape. A Digital Surface Model Light Detection and Ranging (LiDAR) dataset processing and a GIS model was performed to determine landscape quality (aesthetic and ecological) and landforms with similar characteristics for the road layout, and the cumulative viewshed of potential drivers and observers in the area surrounding the new motorway. The main contributions of this research to current scientific knowledge in the field of environmental impact assessment for road corridors and layouts design are four. First, the analysis of 22 Informative Studies on road planning revealed that the methods applied by practitioners for assessing the TCC were not sufficiently standardized due to the lack of uniformity in the cartographic information sources and the TCC valuation methodologies, especially in the analysis of the aesthetic and ecological quality of the landscape. Second, the analysis in this dissertation highlights the importance of multicriteria methods to structure, combine and validate factors that constrain wildlife dispersal movements in the connectivity analysis. Third, the “Generator of Alternative Corridors (GAC)” and “Narrow Corridor Eraser (NCE)” GIS models developed can be applied systematically and on a scientific basis in connectivity analyses to improve existing tools and understand landscape as a network composed of interconnected nodes and links. Thus, alternative corridors with similar probability of use by fauna and without bottlenecks can be obtained by iteratively running GAC and NCE models. Fourth, our case study of new motorway corridors and layouts design innovatively included semi-supervised classification of landforms, filtering of LiDAR point clouds and new 3D road geometry on the Digital Surface Model (DSM). The combined used of LiDAR data processing and geomorphological indices and classifications can help decision-makers assess which road layouts produce lower impacts on the landscape, provide an overall insight into the most commonly applied value judgments, and in conclusion, define which corrective measures should be applied in terms of landscaping, and where.

Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.

Application of Decision Theory methods for a Community of Madrid Soil classification case

A land classification method was designed for the Community of Madrid (CM), which has lands suitable for either agriculture use or natural spaces. The process started from an extensive previous CM study that contains sets of land attributes with data for 122 types and a minimum-requirements method providing a land quality classification (SQ) for each land. Borrowing some tools from Operations Research (OR) and from Decision Science, that SQ has been complemented by an additive valuation method that involves a more restricted set of 13 representative attributes analysed using Attribute Valuation Functions to obtain a quality index, QI, and by an original composite method that uses a fuzzy set procedure to obtain a combined quality index, CQI, that contains relevant information from both the SQ and the QI methods.

The deferral option in the collective dismissal procedure. La opción de aplazamiento en los expedientes de regulación de empleo.

The work in this paper focuses on the integration of the real options theory for organizational projects in the management of Human Resources, and particularly on the inclusion of the deferral option in collective dismissal procedures. This option has been studied and developed to be applied to ?Expediente de regulación de empleo?, which is the legal form existing in Spain for the collective termination of employment contracts and which organizations turn to when confronted with a negative financial situation, as a way of maintaining their viability. Two main issues which it is hoped to resolve are examined: the search for a source of uncertainty to make the deferral option viable for this type of projects, and the development of a procedure to obtain the value of the option and therefore facilitate decision making. The analysis performed has enabled us to state that the volatility of demand is the source of uncertainty that makes the option viable. The procedure developed by the binomial tree, which is determined by the evolution of demand, is the tool that enables the value of the option to be found.