Multi-valued Model Checking extends classical, two-valued model checking to multi-valued logic such as Quasi-Boolean logic. The added expressivity is useful in dealing with such concepts as incompleteness and uncertainty in target systems, while it comes with the cost of time and space. Chechik and others proposed an efficient reduction from multi-valued model checking problems to two-valued ones, but to the authors' knowledge, no study was done for multi-valued bounded model checking. In this paper, we propose a novel, efficient algorithm for multi-valued bounded model checking. A notable feature of our algorithm is that it is not based on reduction of multi-values into two-values; instead, it generates a single formula which represents multi-valuedness by a suitable encoding, and asks a standard SAT solver to check its satisfiability. Our experimental results show a significant improvement in the number of variables and clauses and also in execution time compared with the reduction-based one.

In this paper, the authors focus on upstream transmission in TDMA-based IEEE 802.16j and propose two time slot assignment algorithms to decrease end-to-end transmission latency. One of the proposed algorithms assigns time slots considering the hop count from a gateway node, and the other takes the path from the relay node to the gateway node into account. In addition, a restriction in assigning time slots is introduced to reduce the delay at each relay node. The algorithms with the restriction assign later time slots considering the time slot order of links connecting a relay node. The performance of the proposed algorithms is evaluated through simulation experiments from the viewpoints of frame size and end-to-end transmission latency, and it is confirmed that the proposed algorithms achieve small transmission latency regardless of packet generation rate in the network, and decrease the transmission latency by up to 70% compared with the existing algorithm.

Non-homogeneous Poisson processes (NHPPs) have gained much popularity in actual software testing phases to estimate the software reliability, the number of remaining faults in software and the software release timing. In this paper, we propose a new modeling approach for the NHPP-based software reliability models (SRMs) to describe the stochastic behavior of software fault-detection processes. The fundamental idea is to apply the equilibrium distribution to the fault-detection time distribution in NHPP-based modeling. We also develop efficient parameter estimation procedures for the proposed NHPP-based SRMs. Through numerical experiments, it can be concluded that the proposed NHPP-based SRMs outperform the existing ones in many data sets from the perspective of goodness-of-fit and prediction performance.

Cognitive radios are intelligent communications, and are expected to more efficiently utilize the radio channel. Modulation identification is one of the key issues in the cognitive radios. Many works were devoted to the classification of symbol-by-symbol modulations, however, few papers on block modulations have been published. In this paper, an identification error analysis is presented for block orthogonal modulations using General Orthogonal Modulation~(GOM). A symbol error probability is derived for the identified block orthogonal modulation. Numerical results of 4-dimensional block orthogonal modulation are presented with simulation results.

Polar and Spherical Fourier analysis can be used to extract rotation invariant features for image retrieval and pattern recognition tasks. They are demonstrated to show superiorities comparing with other methods on describing rotation invariant features of two and three dimensional images. Based on mathematical properties of trigonometric functions and associated Legendre polynomials, fast algorithms are proposed for multimedia applications like real time systems and large multimedia databases in order to increase the computation speed. The symmetric points are computed simultaneously. Inspired by relative prime number theory, systematic analysis are given in this paper. Novel algorithm is deduced that provide even faster speed. Proposed method are 9–15% faster than previous work. The experimental results on two and three dimensional images are given to illustrate the effectiveness of the proposed method. Multimedia signal processing applications that need real time polar and spherical Fourier analysis can be benefit from this work.

In parallel computing systems using the master/worker model for distributed grid computing, as the size of handling data grows, the increase in the data transmission time degrades the performance. For divisible workload applications, therefore, multiple-round scheduling algorithms have been being developed to mitigate the adverse effect of longer data transmission time by dividing the data into chunks to be sent out in multiple rounds, thus overlapping the times required for computation and transmission. However, a standard multiple-round scheduling algorithm, Uniform Multi-Round (UMR), adopts a sequential transmission model where the master communicates with one worker at a time, thus the transmission capacity of the link attached to the master cannot be fully utilized due to the limits of worker-side capacity. In the present study, a Parallel Transferable Uniform Multi-Round algorithm (PTUMR) is proposed. It efficiently utilizes the data transmission capacity of network links by allowing chunks to be transmitted in parallel to workers. This algorithm divides workers into groups in a way that fully uses the link bandwidth of the master under some constraints and considers each group of workers as one virtual worker. In particular, introducing a Grouping Threshold effectively deals with very heterogeneous workers in both data transmission and computation capacities. Then, the master schedules sequential data transmissions to the virtual workers in an optimal way like in UMR. The performance evaluations show that the proposed algorithm achieves significantly shorter turnaround times (i.e., makespan) compared with UMR regardless of heterogeneity of workers, which are close to the theoretical lower limits.

This paper proposes an iterative maximum a posteriori (MAP) receiver for orthogonal frequency division multiplexing (OFDM) mobile communications under fast-fading conditions. The previous work in [21] developed a MAP receiver based on the expectation-maximization (EM) algorithm employing the differential model, which can allow correlated time-variation of channel impulse responses. In order to make such a MAP receiver more robust against time-variant channels, this paper proposes two new message-passing algorithms derived from factor graphs; subcarrier removal and partial turbo processing. The subcarrier removal estimates the channel frequency response by using all subcarriers other than the targeted subcarrier. Such channel estimate can be efficiently calculated by removing information on the targeted subcarrier from the estimate of the original EM algorithm that uses all the subcarriers. This modification can avoid the repetitive use of incorrectly detected signals for the channel estimation. On the other hand, the partial turbo processing performs symbol-by-symbol channel decoding by using a symbol interleaver. Owing to this process, the current channel estimate, which is more accurate due to the decoding gain, can be used as the initial channel estimate for the next symbol. Computer simulations under fast multipath fading conditions demonstrate that the subcarrier removal and the partial turbo processing can improve the error floor and the convergence speed, respectively, compared to the conventional MAP receiver.

A simplified algorithm for check node processing of extended min-sum (EMS) q-ary LDPC decoders is presented in this letter. Compared with the bubble check algorithm, the so-called dynamic bubble-check (DBC) algorithm aims to further reduce the computational complexity for the elementary check node (ECN) processing. By introducing two flag vectors in ECN processing, The DBC algorithm can use the minimum number of comparisons at each step. Simulation results show that, DBC algorithm uses significantly fewer comparison operations than the bubble check algorithm, and presents no performance loss compared with standard EMS algorithm on AWGN channels.

Information diffusion analysis in social networks is of significance since it enables us to deeply understand dynamic social interactions among users. In this paper, we introduce approaches to discovering information diffusion process in social networks based on process mining. Process mining techniques are applied from three perspectives: social network analysis, process discovery and community recognition. We then present experimental results by using a real-life social network data. The proposed techniques are expected to employ as new analytical tools in online social networks such as blog and wikis for company marketers, politicians, news reporters and online writers.

Visually saliency detection provides an alternative methodology to image description in many applications such as adaptive content delivery and image retrieval. One of the main aims of visual attention in computer vision is to detect and segment the salient regions in an image. In this paper, we employ matrix decomposition to detect salient object in nature images. To efficiently eliminate high contrast noise regions in the background, we integrate global context information into saliency detection. Therefore, the most salient region can be easily selected as the one which is globally most isolated. The proposed approach intrinsically provides an alternative methodology to model attention with low implementation complexity. Experiments show that our approach achieves much better performance than that from the existing state-of-art methods.

In this paper, we propose a method for supervised single-channel speech separation through sparse decomposition using periodic signal models. The proposed separation method employs sparse decomposition, which decomposes a signal into a set of periodic signals under a sparsity penalty. In order to achieve separation through sparse decomposition, the decomposed periodic signals have to be assigned to the corresponding sources. For the assignment of the periodic signal, we introduce clustering using a K-means algorithm to group the decomposed periodic signals into as many clusters as the number of speakers. After the clustering, each cluster is assigned to its corresponding speaker using preliminarily learnt codebooks. Through separation experiments, we compare our method with MaxVQ, which performs separation on the frequency spectrum domain. The experimental results in terms of signal-to-distortion ratio show that the proposed sparse decomposition method is comparable to the frequency domain approach and has less computational costs for assignment of speech components.

Pentacene-based organic field-effect transistors (OFETs) with SiO2 and HfON gate insulators have been fabricated, and the effect of gate insulator on the electrical properties of pentacene-based OFETs and the microstructures of pentacene films were investigated. It was found that the grain size for pentacene film deposited on HfON gate insulator is larger than that for pentacene film deposited on SiO2 gate insulator. Due to the larger grain size, pentacene-based OFET with HfON gate insulator shows better electrical properties compared to pentacene-based OFET with SiO2 gate insulator. Meanwhile, low-temperature (such as 140) fabricated pentacene-based OFET with HfON gate insulator was also investigated. The OFET fabricated at 140 shows a small subthreshold swing of 0.14 V/decade, a large on/off current ratio of 4 104, a threshold voltage of -0.65 V, and a hole mobility of 0.33 cm2/Vs at an operating voltage of -2 V.

In this paper, we analyze the key factors underlying the implementation, evaluation, and optimization of image processing and computer vision algorithms on embedded GPU using OpenGL ES 2.0 shader model. First, we present the characteristics of the embedded GPU and its inherent advantage when compared to embedded CPU. Additionally, we propose techniques to achieve increased performance with optimized shader design. To show the effectiveness of the proposed techniques, we employ cartoon-style non-photorealistic rendering (NPR), speeded-up robust feature (SURF) detection, and stereo matching as our example algorithms. Performance is evaluated in terms of the execution time and speed-up achieved in comparison with the implementation on embedded CPU.

Clustering technology is very important in ad hoc networks and sensor networks from the view point of reducing the traffic load and energy consumption. In this paper, we propose a new structure formation mechanism as a tool for clustering. It meets the key clustering requirements including the use of an autonomous decentralized algorithm and a consideration of the situation of individual nodes. The proposed mechanism follows the framework of autonomous decentralized control based on local interaction, in which the behavior of the whole system is indirectly controlled by appropriately designing the autonomous actions of the subsystems. As an application example, we demonstrate autonomous decentralized clustering for a two-dimensional lattice network model, and the characteristics and adaptability of the proposed method are shown. In particular, the clusters produced can reflect the environmental situation of each node given by the initial condition.

We study the properties of information dissemination over location-aware gossiping networks leveraging location-based real-time communication applications. Gossiping is a promising method for quickly disseminating messages in a large-scale system, but in its application to information dissemination for location-aware applications, it is important to consider the network topology and patterns of spatial dissemination over the network in order to achieve effective delivery of messages to potentially interested users. To this end, we propose a continuous-space network model extended from Kleinberg's small-world model applicable to actual location-based applications. Analytical and simulation-based study shows that the proposed network achieves high dissemination efficiency resulting from geographically neutral dissemination patterns as well as selective dissemination to proximate users. We have designed a highly scalable location management method capable of promptly updating the network topology in response to node movement and have implemented a distributed simulator to perform dynamic target pursuit experiments as one example of applications that are the most sensitive to message forwarding delay. The experimental results show that the proposed network surpasses other types of networks in pursuit efficiency and achieves the desirable dissemination patterns.

We herein investigate the operation stability of the single-electron-pump (SEP) refrigerator with respect to thermal and dimensional fluctuations. The SEP refrigerator was found to successfully demonstrate single-electron extraction and injection at temperatures up to 2 K. Although the dimensional fluctuation in junction capacitance will seriously affect operation, the effect of the gate capacitance fluctuation is unlikely to be severe.

It has been an important issue to deal with risks in business processes for achieving companies' goals. This paper introduces a method for applying a formal method to analysis of risks and control activities in business processes in order to evaluate control activities consistently, exhaustively, and to give us potential to have scientific discussion on the result of the evaluation. We focus on document flows in business activities and control activities and risks related to documents because documents play important roles in business. In our method, document flows including control activities are modeled and it is verified by OTS/CafeOBJ Method that risks about falsification of documents are avoided by control activities in the model. The verification is done by interaction between humans and CafeOBJ system with theorem proving, and it raises potential to discuss the result scientifically because the interaction gives us rigorous reasons why the result is derived from the verification.

This paper describes a blind watermarking scheme through cyclic signal processing. Due to various rapid networks, there is a growing demand of copyright protection for multimedia data. As efficient watermarking of images, there exist two major approaches: a quantization-based method and a correlation-based method. In this paper, we proposes a correlation-based watermarking technique of three-dimensional (3-D) polygonal models using the fast Fourier transforms (FFTs). For generating a watermark with desirable properties, similar to a pseudonoise signal, an impulse signal on a two-dimensional (2-D) space is spread through the FFT, the multiplication of a complex sinusoid signal, and the inverse FFT. This watermark, i.e., spread impulse signal, in a transform domain is converted to a spatial domain by an inverse wavelet transform, and embedded into 3-D data aligned by the principle component analysis (PCA). In the detection procedure, after realigning the watermarked mesh model through the PCA, we map the 3-D data on the 2-D space via block segmentation and averaging operation. The 2-D data are processed by the inverse system, i.e., the FFT, the division of the complex sinusoid signal, and the inverse FFT. From the resulting 2-D signal, we detect the position of the maximum value as a signature. For 3-D bunny models, detection rates and information capacity are shown to evaluate the performance of the proposed method.

The subset sum problem, which is often called as the knapsack problem, is known as an NP-hard problem, and there are several cryptosystems based on the problem. Assuming an oracle for shortest vector problem of lattice, the low-density attack algorithm by Lagarias and Odlyzko and its variants solve the subset sum problem efficiently, when the “density” of the given problem is smaller than some threshold. When we define the density in the context of knapsack-type cryptosystems, weights are usually assumed to be chosen uniformly at random from the same interval. In this paper, we focus on general subset sum problems, where this assumption may not hold. We assume that weights are chosen from different intervals, and make analysis of the effect on the success probability of above algorithms both theoretically and experimentally. Possible application of our result in the context of knapsack cryptosystems is the security analysis when we reduce the data size of public keys.

We developed a flexible-logic-gate single-electron device (SED) in which logic functions can be selected by changing the voltage applied to the control gate. It consists of an array of nanodots with multiple inputs and multiple outputs. Since the gate electrodes couple capacitively to the many dots underneath, complicated characteristics depending on the combination of the gate voltages yield a selectable logic gate when some of the gate electrodes are used as control gates. One of the important issues is how to design the arrangement of nanodots and gate electrodes. In this study, we fabricated a Si nanodot array with two simple input gates and two output terminals, in which each gate was coupled to half of the nanodot array. Even though the device had a very simple input-gate arrangement and just one control gate, we could create a half-adder function through the use of current maps as functions of the input gate voltages. We found that the nanodots evenly coupled capacitively to both input gates played an important role in getting a basic set of logic functions. Moreover, these results guarantee that a more complicated input-gate structure, in which each gate evenly couples many nanodots, will yield more complicated functions.