Fundamenta Informaticae - Volume 107, issue 1

Authors: Cui, Bo | Kari, Lila | Seki, Shinnosuke

Article Type: Research Article

Abstract: In this paper, we introduce the notion of k-comma codes - a proper generalization of the notion of comma-free codes. For a given positive integer k, a k-comma code is a set L over an alphabet Σ with the property that LΣk L ∩ Σ+ LΣ+ = ∅. Informally, in a k-comma code, no codeword can be a subword of the catenation of two other codewords separated by a “comma” of length k. A k-comma code is indeed a code, that is, any sequence of codewords is uniquely decipherable. We extend this notion to that of k-spacer codes, with …commas of length less than or equal to a given k. We obtain several basic properties of k-comma codes and their generalizations, k-comma intercodes, and some relationships between the families of k-comma intercodes and other classical families of codes, such as infix codes and bifix codes. Moreover, we introduce the notion of n-k-comma intercodes, and obtain, for each k ≥ 0, several hierarchical relationships among the families of n-k-comma intercodes, as well as a characterization of the family of 1-k-comma intercodes. Show more

DOI: 10.3233/FI-2011-390

Citation: Fundamenta Informaticae, vol. 107, no. 1, pp. 1-18, 2011

Authors: Hojjat, Hossein | Mousavi, Mohammad Reza | Sirjani, Marjan

Article Type: Research Article

Abstract: SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic …verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC. Show more

Keywords: SystemC, Process Algebra, Formal Verification, mCRL2

DOI: 10.3233/FI-2011-391

Citation: Fundamenta Informaticae, vol. 107, no. 1, pp. 19-42, 2011

Authors: Kammüller, Florian

Article Type: Research Article

Abstract: We use the technique of interactive theorem proving to develop the theory and an enumeration technique for finite idempotent relations. Starting from a short mathematical characterization of finite idempotents defined and proved in Isabelle/HOL, we derive first an iterative procedure to generate all instances of idempotents over a finite set. From there, we develop a more precise theoretical characterization giving rise to an efficient predicate that can be executed in the programming language ML. Idempotent relations represent a very basic, general mathematical concept but the steps taken to develop their theory with the help of Isabelle/HOL are representative for developing …algorithms from a mathematical specification. Show more

Keywords: Formal Specification of Computer Systems, Idempotent Relations, Interactive Theorem Proving, Higher Order Logic

DOI: 10.3233/FI-2011-392

Citation: Fundamenta Informaticae, vol. 107, no. 1, pp. 43-65, 2011

Authors: She, Yanhong | He, Xiaoli | Wang, Guojun

Article Type: Research Article

Abstract: A propositional logic PRL for rough sets was proposed in [1]. In this paper, we initially introduce the concepts of rough (upper, lower) truth degrees on the set of formulas in PRL. Then, by grading the rough equality relations, we propose the concepts of rough (upper, lower) similarity degree. Finally, three different pseudo-metrics on the set of rough formulas are obtained, and thus an approximate reasoning mechanism is established.

Keywords: Rough (upper, lower) truth degree, Rough (upper, lower) similarity degree, Rough (upper, lower) pseudo-metric, Approximate reasoning

DOI: 10.3233/FI-2011-393

Citation: Fundamenta Informaticae, vol. 107, no. 1, pp. 67-83, 2011

Authors: Wieczorkowska, Alicja | Kubera, Elżbieta | Kubik-Komar, Agnieszka

Article Type: Research Article

Abstract: Experiments with recognition of the dominating musical instrument in sound mixes are interesting from the point of view of music information retrieval, but this task can be very difficult if the mixed sounds are of the same pitch. In this paper, we analyse experiments on recognition of the dominating instrument in mixes of same-pitch sounds of definite pitch. Sound from one octave (no. 4 in MIDI notation) have been chosen, and instruments of various types, including percussive instruments were investigated. Support vector machines were used in our experiments, and statistical analysis of the results was also carefully performed. After discussing …the outcomes of these experiments and analyses, we conclude our paper with suggestions regarding directions of possible future research on this subject. Show more

Keywords: music information retrieval, sound recognition

DOI: 10.3233/FI-2011-394

Citation: Fundamenta Informaticae, vol. 107, no. 1, pp. 85-104, 2011

Authors: Xiong, Hu | Qin, Zhiguang | Li, Fagen

Article Type: Research Article

Abstract: Signcryption is a cryptographic primitive that performs digital signature and public key encryption simultaneously, at lower computational costs and communication overhead than signing and encrypting separately. Recently, Yu et al. proposed an identity based signcryption scheme with a claimed proof of security. We show that their scheme is not secure even against a chosen-plaintext attack.

Keywords: Signcryption, Identity-based cryptography, Chosen plaintext attack

DOI: 10.3233/FI-2011-395

Citation: Fundamenta Informaticae, vol. 107, no. 1, pp. 105-109, 2011