toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Intrigila, Benedetto; Melatti, Igor; Tofani, Alberto; Macchiarelli, Guido pdf  doi
openurl 
  Title (down) Computational models of myocardial endomysial collagen arrangement Type Journal Article
  Year 2007 Publication Computer Methods and Programs in Biomedicine Abbreviated Journal  
  Volume 86 Issue 3 Pages 232-244  
  Keywords  
  Abstract Collagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude /net extension is intended to model the stress /strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress /strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size.  
  Address  
  Corporate Author Thesis  
  Publisher Elsevier North-Holland, Inc. Place of Publication New York, NY, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0169-2607 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Imtm07 Serial 82  
Permanent link to this record
 

 
Author Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Leeners, B. pdf  url
doi  openurl
  Title (down) Complete populations of virtual patients for in silico clinical trials Type Journal Article
  Year 2021 Publication Bioinformatics Abbreviated Journal  
  Volume Issue Pages 1-8  
  Keywords  
  Abstract Model-based approaches to safety and efficacy assessment of pharmacological drugs, treatment strategies, or medical devices (In Silico Clinical Trial, ISCT) aim to decrease time and cost for the needed experimentations, reduce animal and human testing, and enable precision medicine. Unfortunately, in presence of non-identifiable models (e.g., reaction networks), parameter estimation is not enough to generate complete populations of Virtual Patient (VPs), i.e., populations guaranteed to show the entire spectrum of model behaviours (phenotypes), thus ensuring representativeness of the trial.We present methods and software based on global search driven by statistical model checking that, starting from a (non-identifiable) quantitative model of the human physiology (plus drugs PK/PD) and suitable biological and medical knowledge elicited from experts, compute a population of VPs whose behaviours are representative of the whole spectrum of phenotypes entailed by the model (completeness) and pairwise distinguishable according to user-provided criteria. This enables full granularity control on the size of the population to employ in an ISCT, guaranteeing representativeness while avoiding over-representation of behaviours.We proved the effectiveness of our algorithm on a non-identifiable ODE-based model of the female Hypothalamic-Pituitary-Gonadal axis, by generating a population of 4 830 264 VPs stratified into 7 levels (at different granularity of behaviours), and assessed its representativeness against 86 retrospective health records from Pfizer, Hannover Medical School and University Hospital of Lausanne. The datasets are respectively covered by our VPs within Average Normalised Mean Absolute Error of 15%, 20%, and 35% (90% of the latter dataset is covered within 20% error).  
  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 1367-4803 ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number MCLab @ davi @ ref10.1093/bioinformatics/btaa1026 Serial 182  
Permanent link to this record
 

 
Author Kuijpers, Ed; Carotenuto, Luigi; Malapert, Jean-Cristophe; Markov-Vetter, Daniela; Melatti, Igor; Orlandini, Andrea; Pinchuk, Ranni pdf  openurl
  Title (down) Collaboration on ISS Experiment Data and Knowledge Representation Type Conference Article
  Year 2012 Publication Proc. of IAC 2012 Abbreviated Journal  
  Volume D.5.11 Issue Pages  
  Keywords  
  Abstract  
  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 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ melatti @ Serial 107  
Permanent link to this record
 

 
Author Leeners, B.; Krueger, T.; Geraedts, K.; Tronci, E.; Mancini, T.; Ille, F.; Egli, M.; Roeblitz, S.; Wunder, D.; Saleh, L.; Schippert, C.; Hengartner, M.P. pdf  url
doi  openurl
  Title (down) Cognitive function in association with high estradiol levels resulting from fertility treatment Type Journal Article
  Year 2021 Publication Hormones and Behavior Abbreviated Journal  
  Volume 130 Issue Pages 104951  
  Keywords Cognition, Estrogen, Estradiol, Fertility treatment, Attention, Cognitive bias  
  Abstract The putative association between hormones and cognitive performance is controversial. While there is evidence that estradiol plays a neuroprotective role, hormone treatment has not been shown to improve cognitive performance. Current research is flawed by the evaluation of combined hormonal effects throughout the menstrual cycle or in the menopausal transition. The stimulation phase of a fertility treatment offers a unique model to study the effect of estradiol on cognitive function. This quasi-experimental observational study is based on data from 44 women receiving IVF in Zurich, Switzerland. We assessed visuospatial working memory, attention, cognitive bias, and hormone levels at the beginning and at the end of the stimulation phase of ovarian superstimulation as part of a fertility treatment. In addition to inter-individual differences, we examined intra-individual change over time (within-subject effects). The substantial increases in estradiol levels resulting from fertility treatment did not relate to any considerable change in cognitive functioning. As the tests applied represent a broad variety of cognitive functions on different levels of complexity and with various brain regions involved, we can conclude that estradiol does not show a significant short-term effect on cognitive function.  
  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 0018-506x ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number MCLab @ davi @ Leeners2021104951 Serial 185  
Permanent link to this record
 

 
Author file  doi
openurl 
  Title (down) Charme Type Conference Article
  Year 2003 Publication Lecture Notes in Computer Science Abbreviated Journal  
  Volume 2860 Issue Pages  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Geist, D.; Tronci, E.  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 3-540-20363-X ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ editor-charme03 Serial 37  
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico pdf  url
doi  openurl
  Title (down) CGMurphi: Automatic synthesis of numerical controllers for nonlinear hybrid systems Type Journal Article
  Year 2013 Publication European Journal of Control Abbreviated Journal European Journal of Control  
  Volume 19 Issue 1 Pages 14-36  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Elsevier North-Holland, Inc. Place of Publication Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0947-3580 ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ melatti @ Serial 114  
Permanent link to this record
 

 
Author Mari, Federico; Tronci, Enrico pdf  doi
openurl 
  Title (down) CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems Type Conference Article
  Year 2007 Publication Hybrid Systems: Computation and Control (HSCC 2007) Abbreviated Journal  
  Volume Issue Pages 399-412  
  Keywords Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS  
  Abstract Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Bemporad, A.; Bicchi, A.; Buttazzo, G.C.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 4416 Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ MarTro07 Serial 92  
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa pdf  doi
openurl 
  Title (down) Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier Type Conference Article
  Year 2004 Publication Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings Abbreviated Journal  
  Volume Issue Pages 214-229  
  Keywords  
  Abstract In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Hu, A.J.; Martin, A.K.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 3312 Series Issue Edition  
  ISSN 3-540-23738-0 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Dimtz04 Serial 87  
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Minichino, Michele; Ciancamerla, Ester; Parisse, Andrea; Tronci, Enrico; Venturini Zilli, Marisa pdf  doi
openurl 
  Title (down) Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier Type Conference Article
  Year 2003 Publication Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings Abbreviated Journal  
  Volume Issue Pages 141-155  
  Keywords  
  Abstract Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Maler, O.; Pnueli, A.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 2623 Series Issue Edition  
  ISSN 3-540-00913-2 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Dimmcptz03 Serial 88  
Permanent link to this record
 

 
Author Pugliese, Rosario; Tronci, Enrico doi  openurl
  Title (down) Automatic Verification of a Hydroelectric Power Plant Type Conference Article
  Year 1996 Publication Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3 Abbreviated Journal  
  Volume Issue Pages 425-444  
  Keywords  
  Abstract We analyze the specification of a hydroelectric power plant by ENEL (the Italian Electric Company). Our goal is to show that for the specification of the plant (its control system in particular) some given properties hold. We were provided with an informal specification of the plant. From such informal specification we wrote a formal specification using the CCS/Meije process algebra formalism. We defined properties using μ-calculus. Automatic verification was carried out using model checking. This was done by translating our process algebra definitions (the model) and μ-calculus formulas into BDDs. In this paper we present the informal specification of the plant, its formal specification, some of the properties we verified and experimental results.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Oxford, UK Editor Gaudel, M.-C.; Woodcock, J.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 1051 Series Issue Edition  
  ISSN 3-540-60973-3 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ fme96 Serial 53  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: