The present paper investigates the current status of the storage times in self‐organized QDs, surveying a variety of heterostructures advantageous for strong electron and/or hole confinement. Experimental data for the electronic properties, such as localization energies and capture cross‐sections, are listed. Based on the theory of thermal emission of carriers from QDs, we extrapolate the values for materials that would increase the storage time at room temperature to more than millions of years. For electron storage, GaSb/AlSb, GaN/AlN, and InAs/AlSb are proposed. For hole storage, GaSb/Al_0.9Ga_0.1As, GaSb/GaP, and GaSb/AlP are promising candidates.

A new approach is presented to improve the classification performance of medical X‐ray images based on the combination of generative and discriminative classification approach. A set of labelled X‐ray images were given from 116 categories of different parts of body and the aim is to construct a classification model. This model was then used to classify any new X‐ray images into one of the predefined categories. The classification task started with extracting local invariant features from all images. A generative model such as probabilistic latent semantic analysis (PLSA) was applied on extracted features in order to provide more stable representation of the images. Subsequently, this representation was used as input to a discriminative support vector machine classifier to construct a classification model. The experimental results were based on ImageCLEF 2007 medical database. The classification performance was evaluated on the entire dataset as well as the class specific level. It was also compared with other classification techniques with various image representations on the same database. The comparison results showed that superior performance has been achieved especially for classes with less number of training images. Thus, only 7 out of 116 classes were left with accuracy rate below 60% as it differs from the results obtained using other classification approaches. This was attained by exploiting the ability of PLSA to generate a better image representation, discriminative for accurate classification and more robust when less training data are available. The total classification rate obtained on the entire dataset is 92.5%.

Medical images form an essential source of information for various important processes such as diagnosis of diseases, surgical planning, medical reference, research and training. Therefore, effective and meaningful search and classification of these images are vital. In this paper, the approaches of content-based image retrieval (CBIR) using low level features such as shape and texture are investigated in order to create a framework that classify medical X-ray image automatically. Gray level Co-occurrence Matrix, Canny Edge Operator, Local Binary Pattern and pixel level information of the images in this work act as image based feature representations which are adopted in our method. The state-of-the-art machine learning method, Support Vector Machine (SVM) is used for classification. In addition, the performance of image classification offered by combining the promising features stated above is investigated. Experimental results using 116 different classes of 11,000 X-ray images showed 90.7% classification accuracy.

Increasing attention has been paid recently to criteria that allow one to conclude that a structure models a linear-time property from the knowledge that no counterexamples exist up to a certain length. These termination criteria effectively turn Bounded Model Checking into a full-fledged verification technique and sometimes result in considerable time savings. In [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] we presented a criterion based on the translation of the linear-time specification into a Büchi automaton. BMC can be terminated if no fair cycle is found up to a given length, and one can prove that no fair cycle exists beyond that length. The maximum length for which counterexamples are explicitly checked is called the termination length; it obviously depends on the model, the property, and the termination criterion. In this paper we improve the criterion of [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] by adding a check that often substantially reduces termination length. Our previous work employed translation to a non-generalized Büchi automaton. Though a well-known technique converts a generalized automaton into that form by composing it with a counter, it has the undesirable effect of considerably lengthening the cycles in the graph to be searched. We propose several alternatives to that approach and compare them experimentally. The translation to automata can be accomplished in more than one way, and in this paper we contrast two of them: one based on the algorithms of [F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In E. A. Emerson and A. P. Sistla, editors, Twelfth Conference on Computer Aided Verification (CAV'00), pages 248–263. Springer-Verlag, Berlin, July 2000. LNCS 1855], and one based on the notion of tight automaton of [E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 415–427. Springer-Verlag, Berlin, 1994. LNCS 818]. The latter yields shorter counterexamples, but the former often leads to earlier termination. In addition, it can help in identifying safety properties, for which termination checks are much more efficient than for the general case. We finally present results on comparing techniques based on cycle detection to the technique of [V. Schuppan and A. Biere. Efficient reduction of finite state model checking to reachability analysis. Software Tools for Technology Transfer, 5(2–3):185–204, Mar. 2004], which converts liveness properties into safety properties by augmentation of the model