Abstract

Abstract
D-down arrow is a new dynamic logic combining regular modalities with the binder constructor typical of hybrid logic, which provides a smooth framework for the stepwise development of reactive systems. Actually, the logic is able to capture system properties at different levels of abstraction, from high-level safety and liveness requirements, to constructive specifications representing concrete processes. The paper discusses its semantics, given in terms of reachable transition systems with initial states, its expressive power and a proof system. The methodological framework is in debt to the landmark work of D. Sannella and A. Tarlecki, instantiating the generic concepts of constructor and abstractor implementations by standard operators on reactive components, e.g. relabelling and parallel composition, as constructors, and bisimulation for abstraction.

Abstract
The increasing penetration of renewable energy sources characterized by a high degree of variability and uncertainty is a complex challenge for network operators that are obligated to ensure their connection while keeping the quality and security of supply. In order to deal with this variable behavior and forecast uncertainty, the distribution networks are equipped with flexible distributed energy resources capable of adjusting their operating point to avoid technical issues (voltage problems, congestion, etc.). Within this paradigm, the flexibility that, in fact, can be provided by such resources, needs to be estimated/forecasted up to the transmission network node (primary substation) and requires new tools for TSO/DSO coordination. This paper addresses this topic by developing a methodology capable of finding the flexibility area while taking into account the technical grid constraints. The proposed approach is based on the formulation of a single optimization problem which is run several times, according with the expected precision for the flexibility area estimation. To each optimization problem run, a different objective function belonging to a family of straight lines is assigned. This allows exploring the active and reactive power flow limits at the TSO/DSO boundary nodes - which define the flexibility area. The effectiveness of the proposed model has been evaluated on two test networks and the results suggest a step forward in the TSO/DSO coordination field. Nevertheless, further investigations to study the effect of assets with discrete control nature (e.g., on load tap changers - OLTC, capacitor banks) on the occurrence of disjoint flexibility areas should be carried.

Abstract
Background: Simplified projected aortic valve area (EOA(proj)) is a valuable echocardiographic parameter in the evaluation of low flow low gradient aortic stenosis (LFLG AS). Its widespread use in clinical practice is hampered by the laborious process of flow rate (Q) calculation. Objetive: This study proposes a less burdensome, alternative method of Q calculation to be incorporated in the original formula of EOA(proj) and measures the agreement between the new proposed method of EOA(proj) calculation and the original one. Methods: Retrospective observational single-institution study that included all consecutive patients with classic LFLG AS that showed a Q variation with dobutamine infusion >= vertical bar 15 vertical bar% by both calculation methods. Results: Twenty-two consecutive patients with classical LFLG AS who underwent dobutamine stress echocardiography were included. Nine patients showed a Q variation with dobutamine infusion calculated by both classical and alternative methods >= vertical bar 15 vertical bar% and were selected for further statistical analysis. Using the Bland-Altman method to assess agreement we found a systematic bias of 0,037 cm(2) (95% CI 0,004 -0,066), meaning that on average the new method overestimates the EOA(proj) in 0,037 cm(2) compared to the original method. The 95% limits of agreement are narrow (from -0,04 cm(2) to 0,12 cm(2)), meaning that for 95% of individuals, EOA(proj) calculated by the new method would be between 0,04 cm(2) less to 0,12 cm(2) more than the EOA(proj) calculated by the original equation. Conclusion: The bias and 95% limits of agreement of the new method are narrow and not clinically relevant, supporting the potential interchangeability of the two methods of EOA(proj) calculation. As the new method requires less additional measurements, it would be easier to implement in clinical practice, promoting an increase in the use of EOA(proj).

Abstract

Abstract
Lung cancer diagnosis is made by radiologists through nodule search in chest Computed Tomography (CT) scans. This task is known to be difficult and prone to errors that can lead to late diagnosis. Although Computer-Aided Diagnostic (CAD) systems are promising tools to be used in clinical practice, experienced radiologists continue to perform better diagnosis than CADs. This paper proposes a methodology for characterizing the radiologist's gaze during nodules search in chest CT scans. The main goals are to identify regions that attract the radiologists' attention, which can then be used for improving a lung CAD system, and to create a tool to assist radiologists during the search task. For that purpose, the methodology processes the radiologists' gaze and their mouse coordinates during the nodule search. The resulting data is then processed to obtain a 3D gaze path from which relevant attention studies can be derived. To better convey the found information, a reference model of the lung that eases the communication of the location of relevant anatomical/pathological findings is also proposed. The methodology is tested on a set of 24 real-practice gazes, recorded via an Eye tracker, from 3 radiologists.