Yoshiaki KAMIYA Yasushi MURAKAMI Wataru CHUJO Masayuki FUJISE
This paper proposes a new type of optically controlled BFN (beam forming network), an electro-optic BFN using an optical waveguide structure. In this BFN, antenna beam forming is performed using conventional optical variable phase shifters and conventional optical variable directional couplers. An electro-optic BFN can easily utilize monolithic integration capability that will be advantageous to microwave stabilization. In order to discuss practical applicability, microwave characteristics and beam forming characteristics were examined using an experimental BFN fabricated on a LiNbO3 substrate. Resulting from electro-optic lightwave control, linear phase shifting and variable amplitude distribution were measured at various microwave frequencies. Without any other control except for optical offset frequency locking and applying constant voltages, typical short term fluctuation in L-band microwave was measured to be within 3 degreesp-p in phase and 2.5 dBp-p in amplitude, respectively. For the first time, an electro-optic BFN was successful in performing beam forming in an L-band array antenna as well as coaxial cables. It was also verified that radiation pattern measured in 60 degree beam steering using the experimental BFN was comparable to that calculated using conventional microwave BFNs. The experimental results show the feasibility of utilizing an electro-optic BFN in future advanced microwave/millimeter-wave array antenna systems.
We compared--for the same propagation conditions and parameters--the performances of distributed dynamic channel assignment (DDCA) strategies and the performance of fixed channel assignment (FCA). This comparison quantitatively showed the effects of DDCA strategies in increasing spectrum efficiency. It also showed that using DDCA with transmitter power control (TPC) increases the system capacity to 3 4 times what it is with FCA and to 1.4 1.8 times what it is when using DDCA without TPC. We also evaluated the blocking rate and the interference probability for the inside of a cell and found that these are generally much higher close to the cell border than they are near the base station.
Hiroaki KIKUCHI Masao MUKAIDONO
A P-Fuzzy Switching Function is a meaningful class of fuzzy switching functions that is representable by a logic formula consisting of prime implicants. This paper aima at extracting knowledge represented as prime implicants from a given learning data. The main results are the necessary and sufficient conditions for the learning data to be representable with P-fuzzy switching functions, and to be determined by unique logic formula.
The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.
In this paper, we evaluate the performance of handoff schemes in microcellular personal communication systems (PCS) which cater to both pedestrian and vehicular users. Various performance parameters, including blocking of new calls,channel utilization, handoff blocking and call termination probabilities for each user type are evaluated. We study different queuing disciplines for handoff calls and their impact on system performance. We also study the tradeoff in handoff blocking and call termination probabilities between user types as the handoff traffic carried by the system from each user type is varied.
Sérgio V. CAMPOS Edmund M. CLARKE Wilfredo MARRERO Marius MINEA Hiromi HIRAISHI
This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.
Yoshiaki KAKUDA Hideki YUKITOMO Shinji KUSUMOTO Tohru KIKUNO
Conformance testing techniques are required for the efficient production of reliable communication protocols. A lot of conformance testing techniques have been developed. However, most of them can only decide whether an implemented protocol conforms to its specification. That is, the exact locations of faults are not determined by them. This paper presents some conditions that enable to find locations of multiple faults, and then proposes a test sequence generation technique under such conditions. The correctness proof and complexity analysis of the proposed technique are also given. The characteristics of this technique are to generate test sequences based on protocol specifications and interim test results, and to find locations of multiple faults in protocol implementations. Although the length of the test sequence generated by the proposed technique is a little longer than the one generated by the previous one, the class to which the proposed technique can be applied is larger than that to which the previous one can be applied.
Katsumi SUIZU Toshiyuki OGAWA Kazuyasu FUJISHIMA
Ever increasing demand for higher bandwidth memories, which is fueled by multimedia and 3D graphics, seems to be somewhat satisfied with various emerging memory solutions. This paper gives a review of these emerging DRAM architectures and a performance comparison based on a condition to let the readers have some perspectives of the future and optimized graphics systems.
In this paper, we present an analysis of a high-speed slotted ring with a single packet buffer at each station. Assuming that distances between stations affect the network performance only through the sum of themselves (this will be called the "lumpability assumption"), we introduce a model system called the lumped model in which stations are aggregated at a single point on the ring with their relative positions preserved. At the instant when each slot visits the aggregated point of the lumped model, we build a Markov chain by recording the system state of buffers and slots. From the steady state probabilities of the Markov chain, we obtain the mean waiting time and the blocking probability of each station. It will be shown analytically and by simulation that the analysis based on the lumped model yields accurate results for various network conditions.
Chang-Sheng YANG Hideki KASUYA
Three-dimensional vocal tract shapes of a male, a female and a child subjects are measured from magnetic resonance (MR) images during sustained phonation of Japanese vowels /a, i, u, e, o/. Non-uniform dimensional differences in the vocal tract shapes of the subjects are quantitatively measured. Vocal tract area functions of the female and child subjects are normalized to those of the male on the basis of non-uniform and uniform scalings of the vocal tract length and compared with each other. A comparison is also made between the formant frequencies computed from the area functions normalized by the two different scalings. It is suggested by the comparisons that non-uniformity in the vocal tract dimensions is not essential in the normalization of the five Japanese vowels.
Hideaki OKAZAKI Hideo NAKANO Takehiko KAWASE
A parallel blower system is quite familiar in hydraulic machine systems and quite often employed in many process industries. It is dynamically dual to the fundamental functional element of digital computer, that is, the flip-flop circuit, which was extensively studied by Moser. Although the global dynamic behaviour of such systems has significant bearing upon system operation, no substantial study reports have hitherto been presented. Extensive research concern has primarily been concentrated upon the local stability of the equilibrium point. In the paper, a piecewise linear model is used to analytically and numerically investigate its manifold global dynamic behaviour. To do this, first the Poincar
Paul R. STAUFFER Marco LEONCINI Vinicio MANFRINI Guido Biffi GENTILI Chris J. DIEDERICH David BOZZO
Electromagnetic radiation patterns of planar 915MHz Dual Concentric Conductor (DCC) antennas were investigated with theoretical finite difference time domain (FDTD) analyses and experimental measurements of power deposition in a homogeneous lossy dielectric load. Power deposition (SAR) patterns were characterized by scanning an electric field sensor in front of the radiating aperture 1 cm deep in liquid "muscle tissue" phantom. Results showed close agreement between the theoretical simulations and measured SAR patterns for a 3.5cm square aperture. Additional SAR measurements demonstrated the ability to vary aperture size from 3.5-6cm with minimal change in shape of the power deposition pattern. Both analyses indicated that effective power deposition (50% SARmax) extends to the periphery of the square apertures. These data support the conclusion that the DCC aperture constitutes an improved radiator to be used as the functional building block of larger array applicators which are required for adjustable heating of large superficial tissue regions in the treatment of cancer.
Ryo MIZUTANI Tsutomu MATSUMOTO
Password checking schemes are human identification methods commonly adopted in many information systems. One of their disadvantages is that an attacker who correctly observed an input password can impersonate the corresponding user freely. To overcome it there have been proposed interactive human identification schemes. Namely, a human prover who has a secret key is asked a question by a machine verifier, who then checks if an answer from the prover matches the question with respect to the key. This letter examines such a scheme that requires relatively less efforts to human provers. By computer experiments this letter evaluates its resistance against a type of attack; after observing several pairs of questions and correct answers how successfully can an attacker answer the next question?
This paper considers properties of language classes with finite elasticity in the viewpoint of set theoretic operations. Finite elasticity was introduced by Wright as a sufficient condition for language classes to be inferable from positive data, and as a property preserved by (not usual) union operation to generate a class of unions of languages. We show that the family of language classes with finite elasticity is closed under not only union but also various operations for language classes such as intersection, concatenation and so on, except complement operation. As a framework defining languages, we introduce restricted elementary formal systems (EFS's for short), called max length-bounded by which any context-sensitive language is definable. We define various operations for EFS's corresponding to usual language operations and also for EFS classes, and investigate closure properties of the family Ge of max length-bounded EFS classes that define classes of languages with finite elasticity. Furthermore, we present theorems characterizing a max length-bounded EFS class in the family Ge, and that for the language class to be inferable from positive data, provided the class is closed under subset operation. From the former, it follows that for any n, a language class definable by max length-bounded EFS's with at most n axioms has finite elasticity. This means that Ge is sufficiently large.
This paper discusses some problems in Molecular Biology for which learning paradigms are strongly desired. We also present a framework of knowledge discovery by PAC-learning paradigm together with its theory and practice developed in our work for discovery from amino acid sequences.
Computational approaches to concept formation often share a top-down, incremental, hill-climbing classification, and differ from each other in the concept representation and quality criteria. Each of them captures part of the rich variety of conceptual knowledge and many are well suited only when the object-attribute distribution is not sparse. Formal concept analysis is a set-theoretic model that mathematically formulates the human understanding of concepts, and investigates the algebraic structure, Galois lattice, of possible concepts in a given domain. Adopting the idea of representing concepts by mutual closed sets of objects and attributes as well as the Galois lattice structure for concepts from formal concept analysis, we propose an approach to concept formation and develop OSHAM, a method that forms concept hierarchies with high utility score, clear semantics and effective even with sparse object-attribute distributions. In this paper we describe OSHAM, and in an attempt to show its performance we present experimental studies on a number of data sets from the machine learning literature.
Program transformation is a kind of optimization techniques for logic programs, which aims at transforming equally a program into an other form by exploiting some properties or information of the program, so as to make the program cheaper to evaluate. In this paper, a new kind of property of logic programs, called reducibility, is exploited in program transformation. A recursive predicate is reducible if the values of some variables in the recursive predicate are independent to the remainder part and can be detached from the predicate after finite times of expansions. After being proved that the semantic notion of reducibility can be replaced by the syntactic notion of disconnectivity of a R-graph, which is a kind of graph model to represent the behavior of formula expansions, an efficient testing and factoring algorithm is proposed. The paper also extends some existed results on compiled formulas of linear sirups, and compares with some related work.
We describe a formal verification algorithm for pipelined processors. This algorithm proves the equivalence between a processor's design and its specifications by using rewriting of recursive functions and a new type of mathematical induction: extended recursive induction. After the user indicates only selectors in the design, this algorithm can automatically prove processors having more than 10(1010) states. The algorithm is manuary applied to benchmark processors with pipelined control, and we discuss how data width, memory size, and the numbers of pipeline stages and instructions influence the computation cost of proving the correctness of the processors. Further, this algorithm can be used to generate a pipeline invariant.
Toshiko KIKUCHI Takahide MATSUOKA Toshiaki TAKEDA Koichiro KISHI
We reported that a competitive learning neural network had the ability of self-organization in the classification of questionnaire survey data. In this letter, its self-organized learning was evaluated by means of mutual information. Mutual information may be useful to find efficently the network which can give optimal classification.
In the actual sound environmental systems, it seems to be essentially difficult to exactly evaluate a whole probability distribution form of its response fluctuation, owing to various types of natural, social and human factors. We have reported a unified probability density expression in the standard expansion form of Hermite type orthonormal series taking a well-known Gaussian probability density function (abbr. p.d.f.) as the basis for generally evaluating non-Gaussian, non-linear correlation and/or non-stationary properties of the fluctuation phenomenon. However, in the real sound environment, there still remain many actual problems on the necessity of improving the above standard type probability expression for practical use. First, a central point in this paper is focused on how to find a new probabilistic theory of practically evaluating the variety and complexity of the actual random fluctuations, especially through newly introducing an equvivalence transformation toward the standard type probability expression mentioned above in the expansion form of Hermite type orthonormal series. Then, the effectiveness of the proposed theory has been confirmed experimentally too by applying it to the actual problems on the response probability evaluation of various sound insulation systems in an acoustic room.