Informatica

In this article we present the general architecture of a hybrid neuro-symbolic system for the selection and stepwise elimination of predictor variables and non-relevant individuals for the construction of a model. Our purpose is to design tools for extracting the relevant variables and the relevant individuals for an automatic training from data. The objective is to reduce the complexity of storage, therefore the complexity of calculation, and to gradually improve the performance of ordering, that is to say to arrive at a good quality training.

In this paper, the relative multidimensional scaling method is investigated. This method is designated to visualize large multidimensional data. The method encompasses application of multidimensional scaling (MDS) to the so-called basic vector set and further mapping of the remaining vectors from the analyzed data set. In the original algorithm of relative MDS, the visualization process is divided into three steps: the set of basis vectors is constructed using the k-means clustering method; this set is projected onto the plane using the MDS algorithm; the set of remaining data is visualized using the relative mapping algorithm. We propose a modification, which differs from the original algorithm in the strategy of selecting the basis vectors. The experimental investigation has shown that the modification exceeds the original algorithm in the visualization quality and computational expenses. The conditions, where the relative MDS efficiency exceeds that of standard MDS, are estimated.

In this paper, the information theory interpreted as the neural network systems of the brain is considered for information conveying and storing. Using the probability theory and specific properties of the neural systems, some foundations are presented. The neural network model proposed and computational experiments allow us to draw a conclusion that such an approach can be applied in storing, coding, and transmission of information.

The rapid development of network technologies has made the web a huge information source with its own characteristics. In most cases, traditional database-based technologies are no longer suitable for web information processing and management. For effectively processing and managing web information, it is necessary to reveal intrinsic relationships/structures among concerned web information objects such as web pages. In this work, a set of web pages that have their intrinsic relationships is called a web page community. This paper proposes a matrix-based model to describe relationships among concerned web pages. Based on this model, intrinsic relationships among pages could be revealed, and in turn a web page community could be constructed. The issues that are related to the application of the model are deeply investigated and studied. The concepts of community and intrinsic relationships, as well as the proposed matrix-based model, are then extended to other application areas such as biological data processing. Some application cases of the model in a broad range of areas are presented, demonstrating the potentials of this matrix-based model.

We propose an Identity Based Strong Designated Verifier Signature (IBSDVS) scheme using bilinear pairings. Designated Verifier Signature finds application in e-voting, auctions and call for tenders. We prove that the scheme is secure against existential forgery under adaptively chosen message and identity attack in random oracle model. We also show that the problem of delegatability does not exist in our scheme.

The method for calculating the specific conductivity tensor of an anisotropically conductive medium, proposed in this paper, distinguishes itself by the simplicity of physical measurements: it suffices to make an equally thick rectangle-shaped sample with four electrodes fixed on its sides and to take various measurements of current intensity and differences of potentials. The necessary mathematical calculations can be promptly performed, even without using a complex computing technique. The accuracy of the results obtained depends on the dimensions of the sample and on the ratios of the conductivity tensor components.

A technique to improve an eye cataract early detection and quantitative evaluation of maturity using ultrasound was investigated. A broadband coherent signal, backscattered from an eye lens tissue, was digitized, recorded and processed. A new parameter – lens quality was proposed for the human eye cataract quantitative evaluation. Lens quality reflects two phenomena of ultrasound interaction with lens tissue – attenuation and scattering. Digital technique for echo-signal energy and time frequency analysis was applied, ultrasound waves scattering strength and spectral slope was calculated.

In this paper an exact and complete analysis of the Lloyd–Max's algorithm and its initialization is carried out. An effective method for initialization of Lloyd–Max's algorithm of optimal scalar quantization for Laplacian source is proposed. The proposed method is very simple method of making an intelligent guess of the starting points for the iterative Lloyd–Max's algorithm. Namely, the initial values for the iterative Lloyd–Max's algorithm can be determined by the values of compandor's parameters. It is demonstrated that by following that logic the proposed method provides a rapid convergence of the Lloyd–Max's algorithm.

Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The approach eliminates unneeded variables using program slicing technique, and then automatically extracts an initial abstract model from C source code using predicate abstraction and theorem proving. In order to reduce time complexities, we partition the set of candidate predicates into subsets, and construct abstract model independently. On the basis of a counterexample-guided abstraction refinement scheme, the abstraction refines incrementally until the specification is either satisfied or refuted. Our methods can be extended to verifying concurrency C programs by parallel composition.

This paper considers Lur'e type descriptor systems (LDS). The concept of strongly absolute stability is defined for LDS and such a notion is a generalization of absolute stability for Lur'e type standard state-space systems (LSS). A reduced-order LSS is obtained by a standard coordinate transformation and it is shown that the strongly absolute stability of the LDS is equivalent to the absolute stability of the reduced-order LSS. By a generalized Lyapunov function, we derive an LMIs based strongly absolute stability criterion. Furthermore, we present the frequency-domain interpretation of the criterion, which shows that the criterion is a generalization of the classical circle criterion. Finally, numerical examples are given to illustrate the effectiveness of the obtained results.