Abstract: Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system.

Abstract: The aim of this work is to propose an approach to monitor and protect Electric Power System by learning normal system behaviour at substations level, and raising an alarm signal when an abnormal status is detected; the problem is addressed by the use of autoassociative neural networks, reading substation measures. Experimental results show that, through the proposed approach, neural networks can be used to learn parameters underlaying system behaviour, and their output processed to detecting anomalies due to hijacking of measures, changes in the power network topology (i.e. transmission lines breaking) and unexpected power demand trend.

Abstract: Stress is a risk factor for impaired general, mental and reproductive health. The role of physiological and supraphysiological estradiol concentrations in stress perception and stress processing is less well understood. We therefore, conducted a prospective observational study to investigate the association between estradiol, stress perception and stress-related cognitive performance within serial measurements either during the natural menstrual cycle or during fertility treatment, where estradiol levels are strongly above the physiological level of a natural cycle and consequently, represent a good model to study dose-dependent effects of estradiol. Data from 44 women receiving in vitro fertilization at the Department of Reproductive Endocrinology in Zurich, Switzerland was compared to data from 88 women with measurements during their natural menstrual cycle. The german version of the Perceived Stress Questionnaire (PSQ) and the Cognitive Bias Test (CBT), in which cognitive performance is tested under time stress were used to evaluate subjective and functional aspects of stress. Estradiol levels were investigated at four different time points during the menstrual cycle and at two different time points during a fertility treatment. Cycle phase were associated with PSQ worry and cognitive bias in normally cycling women, but different phases of fertility treatment were not associated with subjectively perceived stress and stress-related cognitive bias. PSQ lack of joy and PSQ demands related to CBT in women receiving fertility treatment but not in women with a normal menstrual cycle. Only strong changes of the estradiol level during fertility treatment were weakly associated with CBT, but not with subjectively experienced stress. Our research emphasises the multidimensional character of stress and the necessity to adjust stress research to the complex nature of stress perception and processing. Infertility is associated with an increased psychological burden in patients. However, not all phases of the process to overcome infertility do significantly increase patient stress levels. Also, research on the psychological burden of infertility should consider that stress may vary during the different phases of fertility treatment.

Abstract: Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool.