Wyniki wyszukiwania - BazTech

1

An alternative 3D numerical method to study the biomechanical behaviour of the human inner ear semicircular canal

Santos C. F., Belinha J., Gentil F., Parente M., Jorge R. N.

Acta of Bioengineering and Biomechanics

|

2017

|

Vol. 19, no. 1

3--15

EN

Purpose: The vestibular system is the part of the inner ear responsible for balance. Vertigo and dizziness are generally caused by vestibular disorders and are very common symptoms in people over 60 years old. One of the most efficient treatments at the moment is vestibular rehabilitation, permitting to improve the symptoms. However, this rehabilitation therapy is a highly empirical process, which needs to be enhanced and better understood. Methods: This work studies the vestibular system using an alternative computational approach. Thus, part of the vestibular system is simulated with a three dimensional numerical model. Then, for the first time using a combination of two discretization techniques (the finite element method and the smoothed particle hydrodynamics method), it is possible to simulate the transient behavior of the fluid inside one of the canals of the vestibular system. Results: The obtained numerical results are presented and compared with the available literature. The fluid/solid interaction in the model occurs as expected with the methods applied. The results obtained with the semicircular canal model, with the same boundary conditions, are similar to the solutions obtained by other authors. Conclusions: The numerical technique presented here represents a step forward in the biomechanical study of the vestibular system, which in the future will allow the existing rehabilitation techniques to be improved.

2

Numerical study of Hough technique in surgery of otosclerosis, using the finite element method

Gentil F., Parente M., Martins P., Santos C., Almeida E., Ferreira A., Natali R.

Acta of Bioengineering and Biomechanics

|

2015

|

Vol. 17, no. 4

149--153

EN

Purpose: Otosclerosis is a metabolic bone disease of the otic capsule that can cause the stapes fixation, resulting in conductive hearing loss or, in a profound sensorineural deafness threshold. Surgery is one of the possible treatments for the otosclerosis. To repair small focus of otosclerosis in the anterior crus of the stapes, in 1960, Hough suggested the implementation of a technique in which part of the anterior crus is fractured and the stapes turned. As a result, the posterior crus of the stapes is the only connection with the inner ear. In this work, the outcome of Hough’s surgical technique was simulated. Methods: Based on computerized images, a finite element model of middle ear ossicles and tympanic membrane was created, as well as a model where the stapes has changed. The discretization of the tridimensional solid model was made using the ABAQUS software. The mechanical properties used were taken from the literature and adequate boundary conditions were applied. Results: The results obtained with the Hough technique simulation were compared with a representative model of the normal ear, taking into account the displacements obtained on the central part of the stapes footplate and the maximum principal stress in the stapes crus. Conclusions: The results obtained are closer to the normal ear model, therefore Hough technique stands out as a good option to correct small focus of otosclerosis.

3

Graded Alternating-Time Temporal Logic

Faella M., Napoli M., Parente M.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

189-210

EN

Recently, temporal logics such as μ-calculus and Computational Tree Logic, CTL, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. In both these settings, graded modalities enrich the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k. Both μ-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we study how graded modalities may affect specification languages for open systems. We extend the Alternating-time Temporal Logic (ATL) introduced by Alur et al., that is a derivative of CTL interpreted on game structures, rather than transition systems. We solve the model-checking problem in the concurrent and turn-based settings, proving its PTIME-completeness. We present, and compare with each other, two different semantics: the first seems suitable to off-line synthesis applicationswhile the secondmay find application in the verification of fault-tolerant controllers. We also study the case where players can only employ memoryless strategies, showing that also in this case the model-checking problem is in PTIME.

4

Model Checking for Graded CTL

Ferrante A., Napoli M., Parente M.

Fundamenta Informaticae

|

2009

|

Vol. 96, nr 3

323-339

EN

Recently, complexity issues related to the decidability of the μ-calculus, when the universal and existential quantifiers are augmented with graded modalities, have been investigated by Kupfermann, Sattler and Vardi ([19]). Graded modalities refer to the use of the universal and existential quantifiers with the added capability to express the concept of at least k or all but k, for a non-negative integer k. In this paper we study the Computational Tree Logic CTL, a branching time extension of classical modal logic, augmented with graded modalities and investigate the complexity issues with respect to the model-checking problem. We consider a system model represented by a Kripke structure K and give an algorithm to solve the model-checking problem running in time [...] which is hence tight for the problem (here φ is the number of temporal and boolean operators and does not include the values occurring in the graded modalities). In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples to a specification φgiven in CTL. However, these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both NP-hard and coNP-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of graded-CTL, and have proved that the model-checking problem is solvable in polynomial time.