| |
Records |
Links |
|
Author |
Intrigila, Benedetto; Melatti, Igor; Tofani, Alberto; Macchiarelli, Guido |
|
| |
Title |
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 |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico |
|
| |
Title |
Exploiting Hub States in Automatic Verification |
Type |
Conference Article |
| |
Year |
2005 |
Publication |
Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
54-68 |
|
| |
Keywords |
|
|
| |
Abstract |
In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur$\varphi$ verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur$\varphi$ verification algorithm, saving between 16% and 68% (45% on average) in computation time. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
D.A. Peled; Y.-K. Tsay |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
3707 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-29209-8 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Dimt04 |
Serial |
83 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier |
Type |
Conference Article |
| |
Year |
2003 |
Publication |
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
394-409 |
|
| |
Keywords |
|
|
| |
Abstract |
In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present 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 handle 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 |
Geist, D.; Tronci, E. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2860 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Dimtz03 |
Serial |
84 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier |
Type |
Conference Article |
| |
Year |
2003 |
Publication |
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
277-282 |
|
| |
Keywords |
|
|
| |
Abstract |
We present a verification algorithm that can automatically switch from RAM based verification to disk based verification without discarding the work done during the RAM based verification phase. This avoids having to choose beforehand the proper verification algorithm. Our experimental results show that typically our integrated algorithm is as fast as (sometime faster than) the fastest of the two base (i.e. RAM based and disk based) verification algorithms. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
Geist, D.; Tronci, E. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2860 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ DIMTZ03a |
Serial |
85 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso |
|
| |
Title |
Xere: Towards a Natural Interoperability between XML and ER Diagrams |
Type |
Conference Article |
| |
Year |
2003 |
Publication |
Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
356-371 |
|
| |
Keywords |
|
|
| |
Abstract |
XML (eXtensible Markup Language) is becoming the standard format for documents on Internet and is widely used to exchange data. Often, the relevant information contained in XML documents needs to be also stored in legacy databases (DB) in order to integrate the new data with the pre-existing ones. In this paper, we introduce a technique for the automatic XML-DB integration, which we call Xere. In particular we present, as the first step of Xere, the mapping algorithm which allows the translation of XML Schemas into Entity-Relationship diagrams. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
Pezzè, M. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2621 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-00899-3 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Ddimp03 |
Serial |
86 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico |
|
| |
Title |
Automatic Synthesis of Robust Numerical Controllers |
Type |
Conference Article |
| |
Year |
2007 |
Publication |
Icas '07 |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
4 |
|
| |
Keywords |
|
|
| |
Abstract |
A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the well-known CMurphi verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Computer Society |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
0-7695-2859-5 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Dmtimt07 |
Serial |
89 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry |
|
| |
Title |
Model Checking Nash Equilibria in MAD Distributed Systems |
Type |
Conference Article |
| |
Year |
2008 |
Publication |
FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
1-8 |
|
| |
Keywords |
Model Checking, MAD Distributed System, Nash Equilibrium |
|
| |
Abstract |
We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Press |
Place of Publication |
Piscataway, NJ, USA |
Editor |
Cimatti, A.; Jones, R. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-1-4244-2735-2 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ MarMelSalTroAlvCle08 |
Serial |
93 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems |
Type |
Conference Article |
| |
Year |
2012 |
Publication |
Proceedings of ICSEA 2012, The Seventh International Conference on Software Engineering Advances |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
664-671 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
ThinkMind |
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 @ mari @ icsea12 |
Serial |
98 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems |
Type |
Book Chapter |
| |
Year |
2012 |
Publication |
Theoretical Aspects of Computing – ICTAC 2012 |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
243-258 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer Berlin Heidelberg |
Place of Publication |
|
Editor |
Roychoudhury, A.; D'Souza, M. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
7521 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
978-3-642-32942-5 |
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Mari2012 |
Serial |
99 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Control Software Visualization |
Type |
Conference Article |
| |
Year |
2012 |
Publication |
Proceedings of INFOCOMP 2012, The Second International Conference on Advanced Communications and Computation |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
15-20 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
ThinkMind |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-1-61208-226-4 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ infocomp2012 |
Serial |
100 |
|
| Permanent link to this record |
