Spatio-temporal filtering with morphological operators for robust cell migration estimation in "in-vivo" images

The understanding of the embryogenesis in living systems requires reliable quantitative analysis of the cell migration throughout all the stages of development. This is a major challenge of the "in-toto" reconstruction based on different modalities of "in-vivo" imaging techniques -spatio-temporal resolution and image artifacts and noise. Several methods for cell tracking are available, but expensive manual interaction -time and human resources- is always required to enforce coherence. Because of this limitation it is necessary to restrict the experiments or assume an uncontrolled error rate. Is it possible to obtain automated reliable measurements of migration? can we provide a seed for biologists to complete cell lineages efficiently? We propose a filtering technique that considers trajectories as spatio-temporal connected structures that prunes out those that might introduce noise and false positives by using multi-dimensional morphological operators.

Impact of fire and post-fire management techniques on soil chemical properties

The effects of fire ( Control burned soil) and two emergency stabilisation techniques (grass Seeding and straw Mulching ) on 20 chemical characteristics were evaluated on 0 – 5 cm top-soils sampled 1, 90, 180 and 365 days after an experimental fi re in a steep shrubland of a temperate-humid region (NW Spain). Most part of pH (in H 2 O and KCl) variance was explained by the sampling date. No clear temporal trends were identi fi able for total soil C and N content, likely due to the large SOM pool in these soils; however, changes on soil δ 13 C were explained by the deposition of 13 C-depleted ashes, followed by its progressive erosion, while those on soil δ 15 N were a consequence of fi re induced N outputs. After the fi re, NH 4 + – N, P, Na, K, Mg, Ca, Mn, Cu, Zn and B concentrations increased, while those of NO 3 − – N, Al, Fe and Co did not vary significantly. Despite a significant decline with time, concentrations of Mg, Ca and Mn at the end of the study were still higher than in unburned soil, while those of K, Cu, Zn and B were similar to the pre-fire levels and those of NH 4 + – N, P and Na were below pre-fire values. Mulching and Seeding treatments for burned soil emergency stabilisation had significant effects on soil δ 15 N and extractable K, Mg and Ca, while data were inconclusive for their possible effects on the extractable Al, Fe and Co

Generating descriptions that summarize geospatial and temporal data

Effective data summarization methods that use AI techniques can help humans understand large sets of data. In this paper, we describe a knowledge-based method for automatically generating summaries of geospatial and temporal data, i.e. data with geographical and temporal references. The method is useful for summarizing data streams, such as GPS traces and traffic information, that are becoming more prevalent with the increasing use of sensors in computing devices. The method presented here is an initial architecture for our ongoing research in this domain. In this paper we describe the data representations we have designed for our method, our implementations of components to perform data abstraction and natural language generation. We also discuss evaluation results that show the ability of our method to generate certain types of geospatial and temporal descriptions.

AquaData and AquaGIS: Two computer utilities for temporal and spatial simulations of water-limited yield with AquaCrop.

The crop simulation model AquaCrop, recently developed by FAO can be used for a wide range of purposes. However, in its present form, its use over large areas or for applications that require a large number of simulations runs (e.g., long-term analysis), is not practical without developing software to facilitate such applications. Two tools for managing the inputs and outputs of AquaCrop, named AquaData and AquaGIS, have been developed for this purpose and are presented here. Both software utilities have been programmed in Delphi v. 5 and in addition, AquaGIS requires the Geographic Information System (GIS) programming tool MapObjects. These utilities allow the efficient management of input and output files, along with a GIS module to develop spatial analysis and effect spatial visualization of the results, facilitating knowledge dissemination. A sample of application of the utilities is given here, as an AquaCrop simulation analysis of impact of climate change on wheat yield in Southern Spain, which requires extensive input data preparation and output processing. The use of AquaCrop without the two utilities would have required approximately 1000 h of work, while the utilization of AquaData and AquaGIS reduced that time by more than 99%. Furthermore, the use of GIS, made it possible to perform a spatial analysis of the results, thus providing a new option to extend the use of the AquaCrop model to scales requiring spatial and temporal analyses.

Predicción espacio-temporal de la irradiancia solar global a corto plazo en España mediante geoestadística y redes neuronales artificiales

El enriquecimiento del conocimiento sobre la Irradiancia Solar (IS) a nivel de superficie terrestre, así como su predicción, cobran gran interés para las Energías Renovables (ER) - Energía Solar (ES)-, y para distintas aplicaciones industriales o ecológicas. En el ámbito de las ER, el uso óptimo de la ES implica contar con datos de la IS en superficie que ayuden tanto, en la selección de emplazamientos para instalaciones de ES, como en su etapa de diseño (dimensionar la producción) y, finalmente, en su explotación. En este último caso, la observación y la predicción es útil para el mercado energético, la planificación y gestión de la energía (generadoras y operadoras del sistema eléctrico), especialmente en los nuevos contextos de las redes inteligentes de transporte. A pesar de la importancia estratégica de contar con datos de la IS, especialmente los observados por sensores de IS en superficie (los que mejor captan esta variable), estos no siempre están disponibles para los lugares de interés ni con la resolución espacial y temporal deseada. Esta limitación se une a la necesidad de disponer de predicciones a corto plazo de la IS que ayuden a la planificación y gestión de la energía. Se ha indagado y caracterizado las Redes de Estaciones Meteorológicas (REM) existentes en España que publican en internet sus observaciones, focalizando en la IS. Se han identificado 24 REM (16 gubernamentales y 8 redes voluntarios) que aglutinan 3492 estaciones, convirtiéndose éstas en las fuentes de datos meteorológicos utilizados en la tesis. Se han investigado cinco técnicas de estimación espacial de la IS en intervalos de 15 minutos para el territorio peninsular (3 técnicas geoestadísticas, una determinística y el método HelioSat2 basado en imágenes satelitales) con distintas configuraciones espaciales. Cuando el área de estudio tiene una adecuada densidad de observaciones, el mejor método identificado para estimar la IS es el Kriging con Regresión usando variables auxiliares -una de ellas la IS estimada a partir de imágenes satelitales-. De este modo es posible estimar espacialmente la IS más allá de los 25 km identificados en la bibliografía. En caso contrario, se corrobora la idoneidad de utilizar estimaciones a partir de sensores remotos cuando la densidad de observaciones no es adecuada. Se ha experimentado con el modelado de Redes Neuronales Artificiales (RNA) para la predicción a corto plazo de la IS utilizando observaciones próximas (componentes espaciales) en sus entradas y, los resultados son prometedores. Así los niveles de errores disminuyen bajo las siguientes condiciones: (1) cuando el horizonte temporal de predicción es inferior o igual a 3 horas, las estaciones vecinas que se incluyen en el modelo deben encentrarse a una distancia máxima aproximada de 55 km. Esto permite concluir que las RNA son capaces de aprender cómo afectan las condiciones meteorológicas vecinas a la predicción de la IS. ABSTRACT ABSTRACT The enrichment of knowledge about the Solar Irradiance (SI) at Earth's surface and its prediction, have a high interest for Renewable Energy (RE) - Solar Energy (SE) - and for various industrial and environmental applications. In the field of the RE, the optimal use of the SE involves having SI surface to help in the selection of sites for facilities ES, in the design stage (sizing energy production), and finally on their production. In the latter case, the observation and prediction is useful for the market, planning and management of the energy (generators and electrical system operators), especially in new contexts of smart transport networks (smartgrid). Despite the strategic importance of SI data, especially those observed by sensors of SI at surface (the ones that best measure this environmental variable), these are not always available to the sights and the spatial and temporal resolution desired. This limitation is bound to the need for short-term predictions of the SI to help planning and energy management. It has been investigated and characterized existing Networks of Weather Stations (NWS) in Spain that share its observations online, focusing on SI. 24 NWS have been identified (16 government and 8 volunteer networks) that implies 3492 stations, turning it into the sources of meteorological data used in the thesis. We have investigated five technical of spatial estimation of SI in 15 minutes to the mainland (3 geostatistical techniques and HelioSat2 a deterministic method based on satellite images) with different spatial configurations. When the study area has an adequate density of observations we identified the best method to estimate the SI is the regression kriging with auxiliary variables (one of them is the SI estimated from satellite images. Thus it is possible to spatially estimate the SI beyond the 25 km identified in the literature. Otherwise, when the density of observations is inadequate the appropriateness is using the estimates values from remote sensing. It has been experimented with Artificial Neural Networks (ANN) modeling for predicting the short-term future of the SI using observations from neighbor’s weather stations (spatial components) in their inputs, and the results are promising. The error levels decrease under the following conditions: (1) when the prediction horizon is less or equal than 3 hours the best models are the ones that include data from the neighboring stations (at a maximum distance of 55 km). It is concluded that the ANN is able to learn how weather conditions affect neighboring prediction of IS at such Spatio-temporal horizons.

Plasma dynamics studies by mass spectrometry techniques

We present temporal information obtained by mass spectrometry techniques about the evolution of plasmas generated by laser filamentation in air. The experimental setup used in this work allowed us to study not only the dynamics of the filament core but also of the energy reservoir that surrounds it. Furthermore, valuable insights about the chemistry of such systems like the photofragmentation and/or formation of molecules were obtained. The interpretation of the experimental results are supported by PIC simulations.

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.

Determination of the species generated in atmospheric-pressure laser-induced plasmas by mass spectometry techniques

We present temporal information obtained by mass spectrometry techniques about the evolution of plasmas generated by laser filamentation in air. The experimental setup used in this work allowed us to study not only the dynamics of the filament core but also of the energy reservoir that surrounds it. Furthermore, valuable insights about the chemistry of such systems like the photofragmentation and/or formation of molecules were obtained. The interpretation of the experimental results are supported by PIC simulations.

Spatio-temporal distribution of pyrethroids in soil in Mediterranean paddy fields

Purpose The demand of rice by the increase in population in many countries has intensified the application of pesticides and the use of poor quality water to irrigate fields. The terrestrial environment is one compartment affected by these situations, where soil is working as a reservoir, retaining organic pollutants. Therefore, it is necessary to develop methods to determine insecticides in soil and monitor susceptible areas to be contaminated, applying adequate techniques to remediate them. Materials and methods This study investigates the occurrence of ten pyrethroid insecticides (PYs) and its spatio-temporal variance in soil at two different depths collected in two periods (before plow and during rice production), in a paddy field area located in the Mediterranean coast. Pyrethroids were quantified using gas chromatography?mass spectrometry (GC?MS) after ultrasound-assisted extraction with ethyl acetate. The results obtained were assessed statistically using non-parametric methods, and significant statistical differences (p < 0.05) in pyrethroids content with soil depth and proximity to wastewater treatment plants were evaluated. Moreover, a geographic information system (GIS) was used to monitor the occurrence of PYs in paddy fields and detect risk areas. Results and discussion Pyrethroids were detected at concentrations ?57.0 ng g?1 before plow and ?62.3 ng g?1 during rice production, being resmethrin and cyfluthrin the compounds found at higher concentrations in soil. Pyrethroids were detected mainly at the top soil, and a GIS program was used to depict the obtained results, showing that effluents from wastewater treatment plants (WWTPs) were the main sources of soil contamination. No toxic effects were expected to soil organisms, but it is of concern that PYs may affect aquatic organisms, which represents the worst case scenario. Conclusions A methodology to determine pyrethroids in soil was developed to monitor a paddy field area. The use of water fromWWTPs to irrigate rice fields is one of the main pollution sources of pyrethroids. It is a matter of concern that PYs may present toxic effects on aquatic organisms, as they can be desorbed from soil. Phytoremediation may play an important role in this area, reducing the possible risk associated to PYs levels in soil.