Informatica

In this paper we consider branching time temporal logics of knowledge and belief. These logics involve the discrete time linear temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. The latter operator is interpreted with respect to a version of the bundle semantics. In addition the temporal logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”) and it contains the modality of common knowledge (belief). For these logics we present sequent calculi with a restricted cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness for these calculi are proved.

The objective of this research is to construct parallel models that simulate the behavior of artificial neural networks. The type of network that is simulated in this project is the counterpropagation network and the parallel platform used to simulate that network is the message passing interface (MPI). In the next sections the counterpropagation algorithm is presented in its serial as well as its parallel version. For the latter case, simulation results are given for the session parallelization as well as the training set parallelization approach. Regarding possible parallelization of the network structure, there are two different approaches that are presented; one that is based to the concept of the intercommunicator and one that uses remote access operations for the update of the weight tables and the estimation of the mean error for each training stage.

Deniable authenticated protocol is a new cryptographic authentication protocol that enables a designated receiver to identify the source of a given message without being able to prove the identity of the sender to a third party. Therefore, it can be applied to some particular situations in electronic commerce. In this paper, we formally define the security model for the non-interactive ID-based deniable authentication protocol and present a new efficient ID-based deniable authentication protocol based on RSA assumption. What's more, we also use the techniques from provable security to analyze the security of our proposed protocol.

A generalized group-oriented cryptosystem (GGOC) based on ElGamal cryptosystem was proposed by Yang et al. in 2003. This study shows that if the authorized decryption sets of users are not properly predetermined in Yang et al.'s GGOC, an unauthorized decryption set of users can recover the encrypted message without difficulty. This study also presents an improved protocol to resist such an attack.

Recently, Chen, Chung, and Huang proposed a traceable proxy multisignature scheme based on the elliptic curve cryptosystem. However, this paper shows that the original signers can produce a valid signature as the proxy signer does in the proxy protected scheme. Therefore, Chen et al.'s proxy-protected scheme cannot protect the proxy signer from being forged by the original signers. We further find that the early work of Chen et al. in 2003 suffers the same attack. To overcome this problem, an improved scheme will be presented.

The paper presents, first, the Structural Blanks (SB) approach, then a method to compose loop programs. SB is an approach for expressing computations based on recurrence relations and focuses on data dependencies in loops. The paper presents language constructs and semantics for expressing programs that have complex data dependency patterns. These constructs are expressed using structural “blanks” for computations based on recurrence relations. In SB the recurrence structure and the functional part of a recurrence relation may be described separately. Therefore declarative representation of data dependencies is examined. SB aims at supporting the transformational development and reuse of program modules. The approach deals with two aspects: pragmatics and semantics. In the paper we aim at: (1) developing a theory and language for functional and structural modules, (2) an algorithm for composition of structural modules. The approach is illustrated by toy problems: the Fibonacci function, heat flow, etc. Hence the reuse and verification are viewed as those of, e.g., stacks, queues, bubble sort, etc.

Recently, there are several articles proposed based on Yang and Shieh's password authentication schemes (YS for short) with the following features: (1) A user can choose password freely. (2) The server does not need to maintain a password table. (3) There is no need to involve a trusted third party. Although there were several variants of the YS-like schemes claimed to address the forgery attacks, this paper analyzes their security and shows that they still suffer from forgery attacks. Furthermore, a new scheme based on the concept of message authentication is proposed to foil the forgery attack.

The aim of this paper is to explore some features of the functional test generation problem, and on the basis of the gained experience, to propose a practical method for functional test generation. In the paper presented analysis of random search methods and adjacent stimuli generation allowed formulating a practical method for generating functional tests. This method incorporates the analyzed termination conditions of generation, exploits the advantages of random and deterministic search, as well as the feature that the sets of the selected input stimuli can be merged easily in order to obtain a better set of test patterns.

The paper analyses the problem of ranking accuracy in multiple criteria decision-making (MCDM) methods. The methodology for measuring the accuracy of determining the relative significance of alternatives as a function of the criteria values is developed. An algorithm of the Technique for the Order Preference by Similarity to Ideal Solution (TOPSIS) that applies criteria values' transformation through a normalization of vectors and the linear transformation is considered. A computational experiment is presented, to compare the results of a multiple criteria analysis and the ranking accuracy in a particular situation.

There is presented a technique of transcribing Lithuanian text into phonemes for speech recognition. Text-phoneme transformation has been made by formal rules and the dictionary. Formal rules were designed to set the relationship between segments of the text and units of formalized speech sounds – phonemes, dictionary – to correct transcription and specify stress mark and position. Proposed the automatic transcription technique was tested by comparing its results with manually obtained ones. The experiment has shown that less than 6% of transcribed words have not matched.