Wyniki wyszukiwania - Biblioteka Nauki

1

Model Checking for Graded CTL

100%

Ferrante A. , Napoli M. , Parente M.

|

tom 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.

2

Graded Alternating-Time Temporal Logic

100%

Faella M. , Napoli M. , Parente M.

|

2011

|

tom 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.

3

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

75%

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

|

tom 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.