Home | [1–10] << 11 12 13 14 15 >> |
Records | |||||
---|---|---|---|---|---|
Author | Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto | ||||
Title | A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET | Type | Journal Article | ||
Year | 2013 | Publication | Mobile Information Systems | Abbreviated Journal | Mobile Information Systems |
Volume | 3 | Issue | 9 | Pages | 261-280 |
Keywords | |||||
Abstract | |||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IOS Press | Place of Publication | Editor | ||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1574-017x (Print) 1875-905X (Online) | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | Sapienza @ melatti @ | Serial | 109 | ||
Permanent link to this record | |||||
Author | Leeners, B.; Kruger, T.H.C.; Geraedts, K.; Tronci, E.; Mancini, T.; Ille, F.; Egli, M.; Röblitz, S.; Saleh, L.; Spanaus, K.; Schippert, C.; Zhang, Y.; Hengartner, M.P. | ||||
Title | Lack of Associations between Female Hormone Levels and Visuospatial Working Memory, Divided Attention and Cognitive Bias across Two Consecutive Menstrual Cycles | Type | Journal Article | ||
Year | 2017 | Publication | Frontiers in Behavioral Neuroscience | Abbreviated Journal | |
Volume | 11 | Issue | Pages | 120 | |
Keywords | |||||
Abstract | Background: Interpretation of observational studies on associations between prefrontal cognitive functioning and hormone levels across the female menstrual cycle is complicated due to small sample sizes and poor replicability. Methods: This observational multisite study comprised data of n=88 menstruating women from Hannover, Germany, and Zurich, Switzerland, assessed during a first cycle and n=68 re-assessed during a second cycle to rule out practice effects and false-positive chance findings. We assessed visuospatial working memory, attention, cognitive bias and hormone levels at four consecutive time-points across both cycles. In addition to inter-individual differences we examined intra-individual change over time (i.e., within-subject effects). Results: Oestrogen, progesterone and testosterone did not relate to inter-individual differences in cognitive functioning. There was a significant negative association between intra-individual change in progesterone and change in working memory from pre-ovulatory to mid-luteal phase during the first cycle, but that association did not replicate in the second cycle. Intra-individual change in testosterone related negatively to change in cognitive bias from menstrual to pre-ovulatory as well as from pre-ovulatory to mid-luteal phase in the first cycle, but these associations did not replicate in the second cycle. Conclusions: There is no consistent association between women's hormone levels, in particular oestrogen and progesterone, and attention, working memory and cognitive bias. That is, anecdotal findings observed during the first cycle did not replicate in the second cycle, suggesting that these are false-positives attributable to random variation and systematic biases such as practice effects. Due to methodological limitations, positive findings in the published literature must be interpreted with reservation. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Place of Publication | Editor | |||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1662-5153 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | Sapienza @ mari @ ref10.3389/fnbeh.2017.00120 | Serial | 167 | ||
Permanent link to this record | |||||
Author | Leeners, B.; Krueger, T.H.C.; Geraedts, K.; Tronci, E.; Mancini, T.; Egli, M.; Roeblitz, S.; Saleh, L.; Spanaus, K.; Schippert, C.; Zhang, Y.; Ille, F. | ||||
Title | Associations Between Natural Physiological and Supraphysiological Estradiol Levels and Stress Perception | Type | Journal Article | ||
Year | 2019 | Publication | Frontiers in Psychology | Abbreviated Journal | |
Volume | 10 | Issue | Pages | 1296 | |
Keywords | |||||
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. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Place of Publication | Editor | |||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1664-1078 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | MCLab @ davi @ ref10.3389/fpsyg.2019.01296 | Serial | 178 | ||
Permanent link to this record | |||||
Author | Tortora, L.; Meynen, G.; Bijlsma, J.; Tronci, E.; Ferracuti, S. | ||||
Title | Neuroprediction and A.I. in Forensic Psychiatry and Criminal Justice: A Neurolaw Perspective | Type | Journal Article | ||
Year | 2020 | Publication | Frontiers in Psychology | Abbreviated Journal | |
Volume | 11 | Issue | Pages | 220 | |
Keywords | |||||
Abstract | Advances in the use of neuroimaging in combination with A.I., and specifically the use of machine learning techniques, have led to the development of brain-reading technologies which, in the nearby future, could have many applications, such as lie detection, neuromarketing or brain-computer interfaces. Some of these could, in principle, also be used in forensic psychiatry. The application of these methods in forensic psychiatry could, for instance, be helpful to increase the accuracy of risk assessment and to identify possible interventions. This technique could be referred to as ‘A.I. neuroprediction,’ and involves identifying potential neurocognitive markers for the prediction of recidivism. However, the future implications of this technique and the role of neuroscience and A.I. in violence risk assessment remain to be established. In this paper, we review and analyze the literature concerning the use of brain-reading A.I. for neuroprediction of violence and rearrest to identify possibilities and challenges in the future use of these techniques in the fields of forensic psychiatry and criminal justice, considering legal implications and ethical issues. The analysis suggests that additional research is required on A.I. neuroprediction techniques, and there is still a great need to understand how they can be implemented in risk assessment in the field of forensic psychiatry. Besides the alluring potential of A.I. neuroprediction, we argue that its use in criminal justice and forensic psychiatry should be subjected to thorough harms/benefits analyses not only when these technologies will be fully available, but also while they are being researched and developed. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Place of Publication | Editor | |||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1664-1078 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | MCLab @ davi @ Neuroprediction-2020 | Serial | 180 | ||
Permanent link to this record | |||||
Author | Fischer, S.; Ehrig, R.; Schaefer, S.; Tronci, E.; Mancini, T.; Egli, M.; Ille, F.; Krueger, T.H.C.; Leeners, B.; Roeblitz, S. | ||||
Title | Mathematical Modeling and Simulation Provides Evidence for New Strategies of Ovarian Stimulation | Type | Journal Article | ||
Year | 2021 | Publication | Frontiers in Endocrinology | Abbreviated Journal | |
Volume | 12 | Issue | Pages | 117 | |
Keywords | |||||
Abstract | New approaches to ovarian stimulation protocols, such as luteal start, random start or double stimulation, allow for flexibility in ovarian stimulation at different phases of the menstrual cycle. It has been proposed that the success of these methods is based on the continuous growth of multiple cohorts (“waves”) of follicles throughout the menstrual cycle which leads to the availability of ovarian follicles for ovarian controlled stimulation at several time points. Though several preliminary studies have been published, their scientific evidence has not been considered as being strong enough to integrate these results into routine clinical practice. This work aims at adding further scientific evidence about the efficiency of variable-start protocols and underpinning the theory of follicular waves by using mathematical modeling and numerical simulations. For this purpose, we have modified and coupled two previously published models, one describing the time course of hormones and one describing competitive follicular growth in a normal menstrual cycle. The coupled model is used to test ovarian stimulation protocols in silico. Simulation results show the occurrence of follicles in a wave-like manner during a normal menstrual cycle and qualitatively predict the outcome of ovarian stimulation initiated at different time points of the menstrual cycle. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Place of Publication | Editor | |||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1664-2392 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | MCLab @ davi @ ref10.3389/fendo.2021.613048 | Serial | 189 | ||
Permanent link to this record | |||||
Author | Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B. | ||||
Title | Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins | Type | Journal Article | ||
Year | 2020 | Publication | Abbreviated Journal | Fundamenta Informaticae | |
Volume | 174 | Issue | Pages | 283-310 | |
Keywords | Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation | ||||
Abstract | In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IOS Press | Place of Publication | Editor | ||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1875-8681 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | MCLab @ davi @ | Serial | 187 | ||
Permanent link to this record | |||||
Author | Chen, Q.M.; Finzi, A.; Mancini, T.; Melatti, I.; Tronci, E. | ||||
Title | MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks | Type | Journal Article | ||
Year | 2020 | Publication | Abbreviated Journal | Fundamenta Informaticae | |
Volume | 174 | Issue | Pages | 229-258 | |
Keywords | |||||
Abstract | In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes . As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance ). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IOS Press | Place of Publication | Editor | ||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1875-8681 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | MCLab @ davi @ | Serial | 188 | ||
Permanent link to this record | |||||
Author | Mancini, T.; Melatti, I.; Tronci, E. | ||||
Title | Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification | Type | Journal Article | ||
Year | 2021 | Publication | IEEE Transactions on Software Engineering | Abbreviated Journal | |
Volume | Issue | Pages | 1-1 | ||
Keywords | |||||
Abstract | Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Place of Publication | Editor | |||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1939-3520 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | To appear | Approved | no | ||
Call Number | MCLab @ davi @ ref9527998 | Serial | 191 | ||
Permanent link to this record | |||||
Author | Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | Synthesizing Control Software from Boolean Relations | Type | Journal Article | ||
Year | 2012 | Publication | International Journal on Advances in Software | Abbreviated Journal | Intern. Journal on Advances in SW |
Volume | vol. 5, nr 3&4 | Issue | Pages | 212-223 | |
Keywords | Control Software Synthesis; Embedded Systems; Model Checking | ||||
Abstract | Many software as well digital hardware automatic
synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately, the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper, we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a worst case execution time linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F. Moreover, a formal proof of the proposed algorithm correctness is also shown. Finally, we present experimental results showing effectiveness of the proposed algorithm. |
||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IARIA | Place of Publication | Editor | Luigi Lavazza | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1942-2628 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ melatti @ | Serial | 108 | ||
Permanent link to this record | |||||
Author | Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems | Type | Journal Article | ||
Year | 2013 | Publication | International Journal on Advances in Software | Abbreviated Journal | Intern. Journal on Advances in SW |
Volume | vol. 6, nr 1&2 | Issue | Pages | 155-169 | |
Keywords | Model-based software design; Linear predicates; Hybrid systems | ||||
Abstract | Model based design is particularly appealing in
software based control systems (e.g., embedded software) design, since in such a case system level specifications are much easier to define than the control software behavior itself. In turn, model based design of embedded systems requires modeling both continuous subsystems (typically, the plant) as well as discrete subsystems (the controller). This is typically done using hybrid systems. Mixed Integer Linear Programming (MILP) based abstraction techniques have been successfully applied to automatically synthesize correct-by-construction control software for discrete time linear hybrid systems, where plant dynamics is modeled as a linear predicate over state, input, and next state variables. Unfortunately, MILP solvers require such linear predicates to be conjunctions of linear constraints, which is not a natural way of modeling hybrid systems. In this paper we show that, under the hypothesis that each variable ranges over a bounded interval, any linear predicate built upon conjunction and disjunction of linear constraints can be automatically translated into an equivalent conjunctive predicate. Since variable bounds play a key role in this translation, our algorithm includes a procedure to compute all implicit variable bounds of the given linear predicate. Furthermore, we show that a particular form of linear predicates, namely guarded predicates, are a natural and powerful language to succinctly model discrete time linear hybrid systems dynamics. Finally, we experimentally show the feasibility of our approach on an important and challenging case study taken from the literature, namely the multi-input Buck DC-DC Converter. As an example, the guarded predicate that models (with 57 constraints) a 6-inputs Buck DC-DC Converter is translated in a conjunctive predicate (with 102 linear constraints) in about 40 minutes. |
||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IARIA | Place of Publication | Editor | Luigi Lavazza | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1942-2628 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ melatti @ | Serial | 115 | ||
Permanent link to this record |