Abstract

Abstract
A reactive model, as studied by D. Gabbay and his collaborators, can be regarded as a graph whose set of edges may be altered whenever one of them is crossed. In this paper we show how reactive models can describe biological regulatory networks and compare them to Boolean networks and piecewise-linear models, which are some of the most common kinds of models used nowadays. In particular, we show that, with respect to the identification of steady states, reactive Boolean networks lie between piecewise linear models and the usual, plain Boolean networks. We also show this ability is preserved by a suitable notion of bisimulation, and, therefore, by network minimisation. © 2019, Springer Nature Switzerland AG.

Abstract
The collection of health and fitness longitudinal data can be used to model disease progression and shape new algorithms to diagnose and predict health hazards. Continuously tracking vital signs, in particular heart rate and skin temperature, can be very informative by using models and algorithms to predict and notify the user about when he might be falling ill. With the current wearable devices and the proper algorithms, the individual can be permanently monitored, which might be much more interesting than a one-off reading comparison with the population average, made by a doctor. It would be possible to intervene earlier and to prevent somebody from becoming seriously ill. From a broader perspective, the knowledge about a user’s health can be considered as an element of that user’s context and be used by context aware applications to provide higher value to the user. After the trivialization of the data acquisition sensors, wearable devices, and raw data, the next logical step is the development of contained software components that can infer and produce knowledge from the raw data. These components and the knowledge they produce can be used by all sorts of applications in order to further customize their usage by a specific user. Customization and context awareness, in regard to health, is a wide field for research and there are a multitude of proposals for models and algorithms. In this review work we searched for software components (frameworks, software libraries, etc.), freely available and that can be used as building blocks for other computer systems by software developers. Copyright

Abstract
This study aimed to characterize vineyard vegetation thorough multi-temporal monitoring using a commercial low-cost rotary-wing unmanned aerial vehicle (UAV) equipped with a consumer-grade red/green/blue (RGB) sensor. Ground-truth data and UAV-based imagery were acquired on nine distinct dates, covering the most significant vegetative growing cycle until harvesting season, over two selected vineyard plots. The acquired UAV-based imagery underwent photogrammetric processing resulting, per flight, in an orthophoto mosaic, used for vegetation estimation. Digital elevation models were used to compute crop surface models. By filtering vegetation within a given height-range, it was possible to separate grapevine vegetation from other vegetation present in a specific vineyard plot, enabling the estimation of grapevine area and volume. The results showed high accuracy in grapevine detection (94.40%) and low error in grapevine volume estimation (root mean square error of 0.13 m and correlation coefficient of 0.78 for height estimation). The accuracy assessment showed that the proposed method based on UAV-based RGB imagery is effective and has potential to become an operational technique. The proposed method also allows the estimation of grapevine areas that can potentially benefit from canopy management operations.

Abstract
In a world where many human lives depend on the correct behavior of software systems, program verification assumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns. © 2018 IEEE.

Abstract
The development of smart mobility initiatives requires specialized and contextualized policies addressing the needs and interests of many stakeholders involved. Since the development of such policies is challenging, there is a need to learn from the experience of many cities around the world offering efficient and successfully adopted smart mobility services. However, in practice, the information provided about such initiatives is shallow and unstructured. To address this issue, we study the state of the art in mobility services, reviewing scientific publications and 42 smart mobility services delivered by nine smart cities around the world, and we propose a taxonomy for planning and designing smart mobility services. The taxonomy provides a common vocabulary to discuss and share information about such services. It comprises eight dimensions: type of services, maturity level, users, applied technologies, delivery channels, benefits, beneficiaries, and common functionality. The contribution of the proposed taxonomy is to serve as a tool for guiding policy makers by identifying a spectrum of mobility services that can be provided, to whom, what technologies can be used to deliver them, and what is the delivered public value so to justify their implementation. In addition, the taxonomy can also assist researchers in further developing the domain. By identifying common functionality, it could also help Information Technology (IT) teams in building and maintaining smart mobility services. Finally, we further discuss usage scenarios of the taxonomy by policy makers, IT staff and researchers.