Tomo-SAR imaging with sparse baselines can be formulated as a sparse signal recovery problem, which suggests the use of the Compressive Sensing (CS) method. In this paper, a novel Tomo-SAR imaging approach based on Sparse Bayesian Learning (SBL) is presented to obtain super-resolution in elevation direction and is validated by simulation results.

The digital logic rewiring technique has been shown to be one of the most powerful logic transformation methods. It has been proven that rewiring is able to further improve some already excellent results on many EDA problems, ranging from logic minimization, partitioning, FPGA technology mappings to final routings. Previous studies have shown that ATPG-based rewiring is one of the most powerful tools for logic perturbation while a graph-based rewiring engine is able to cover nearly one fifth of the target wires with 50 times runtime speedup. For some problems that only require good-enough and very quick solutions, this new rewiring technique may serve as a useful and more practical alternative. In this work, essential elements in graph-based rewiring such as rewiring patterns, pattern size and locality, etc., have been studied to understand their relationship with rewiring performance. A structural analysis on the target-alternative wire pairs discovered by ATPG-based and graph-based engines has also been conducted to analyze the structural characteristics that favor the identification of alternative wires. We have also developed a hybrid rewiring approach that can take the advantages from both ATPG-based and graph-based rewiring. Experimental results suggest that our hybrid engine is able to achieve about 50% of alternative wire coverage when compared with the state-of-the-art ATPG-based rewiring engine with only 4% of the runtime. Through applying our hybrid rewiring approach to the FGPA technology mapping problem, we could achieve similar depth level and look-up table number reductions with much shorter runtime. This shows that the fast runtime of our hybrid approach does not sacrifice the quality of certain rewiring applications.

Visibly pushdown automata (VPA), introduced by Alur and Madhusuan in 2004, is a subclass of pushdown automata whose stack behavior is completely determined by the input symbol according to a fixed partition of the input alphabet. Since it was introduced, VPA have been shown to be useful in various contexts, e.g., as specification formalism for verification and as an automaton model for processing XML streams. However, implementation of formal verification based on VPA framework is a challenge. In this paper, we propose on-the-fly algorithms to test universality and inclusion problems of this automata class. In particular, we first present a slight improvement on the upper bound for determinization of VPA. Next, in order to check universality of a nondeterministic VPA, we simultaneously determinize this VPA and apply the P-automata technique to compute a set of reachable configurations of the target determinized VPA. When a rejecting configuration is found, the checking process stops and reports that the original VPA is not universal. Otherwise, if all configurations are accepting, the original VPA is universal. Furthermore, to strengthen the algorithm, we define a partial ordering over transitions of P-automaton, and only minimal transitions are used to incrementally generate the P-automaton. The purpose of this process is to keep the determinization step implicitly for generating reachable configurations as minimum as possible. This improvement helps to reduce not only the size of the P-automaton but also the complexity of the determinization phase. We implement the proposed algorithms in a prototype tool, named VPAchecker. Finally, we conduct experiments on randomly generated VPA. The experimental results show that the proposed method outperforms the standard one by several orders of magnitude.

Coordinated multi-point processing at multiple base stations can improve coverage, system throughput, and cell-edge throughput for future cellular systems. In this paper, we study the coordinated reception of transmitted signals at multiple MIMO base stations to exploit cooperative diversity. In particular, we propose to employ cooperative multicell automatic repeat request (ARQ) protocol via backhaul links. The attractiveness of this protocol is that processing between coordinated base stations can be made completely transparent to the mobile user, and it improves the mobile user's link reliability and throughput significantly compared to noncooperative ARQ protocol. In our proposed protocol, we consider the scenario where the multicell processing involves one of the following three schemes: decode-and-forward, amplify-and-forward, and compress-and-forward schemes. We derive the average packet error rate and throughput for these cooperative multicell ARQ protocols. Numerical results show that the cooperative multicell ARQ protocols are promising in terms of average packet error rate and throughput. Furthermore, we show that the degree of improvement depends on the type of cooperative multicell ARQ protocol employed and the operating average signal-to-noise ratio of the main and backhaul links.

This paper presents a digital spike map and its learning algorithm of spike-trains. The map is characterized by a swarm of particles on lattice points. As a teacher signal is applied, the algorithm finds a winner particle. The winner and its neighbor particles move in a similar way to the self-organizing maps. A new particle can born and the particle swarm can grow depending on the property of teacher signals. If learning parameters are selected suitably, the map can evolve to approximate a class of teacher signals. Performing basic numerical experiments, the algorithm efficiency is confirmed.

An asynchronous sequential logic spiking neuron is an artificial neuron model that can exhibit various bifurcations and nonlinear responses to stimulation inputs. In this paper, a pulse-coupled system of the asynchronous sequential logic spiking neurons is presented. Numerical simulations show that the coupled system can exhibit various lockings and related nonlinear responses. Then, theoretical sufficient parameter conditions for existence of typical lockings are provided. Usefulness of the parameter conditions is validated by comparing with the numerical simulation results as well as field programmable gate array experiment results.

We determine the autocorrelations of the quaternary sequence over F4 and its modified version introduced by Du et al. [X.N. Du et al., Linear complexity of quaternary sequences generated using generalized cyclotomic classes modulo 2p, IEICE Trans. Fundamentals, vol.E94-A, no.5, pp.1214–1217, 2011]. Furthermore, we reveal a drawback in the paper aforementioned and remark that the proof in the paper by Kim et al. can be simplified.

Main bottleneck of photomosaic algorithm is a search for a best matched image. Unlike several techniques which use fast approximation search for increasing the speed, we propose a parallel framework for fast photomosaic using a programmable GPU. This paper suggests a design of vertex structure for a best match searching on each cell of photomosaic grid and shows a texture representation of image database. The shader programs which are used for searching a best match and rendering image tiles into a display are presented. In addition, a simple duplicate reduction and color correction methods are proposed. Our algorithm not only offers dramatic enhancement of speed, but also always guarantees the 'exact' result.

We propose a novel method of supervised feature projection called class-distance-based discriminant analysis (CDDA), which is suitable for automatic age estimation (AAE) from facial images. Most methods of supervised feature projection, e.g., Fisher discriminant analysis (FDA) and local Fisher discriminant analysis (LFDA), focus on determining whether two samples belong to the same class (i.e., the same age in AAE) or not. Even if an estimated age is not consistent with the correct age in AAE systems, i.e., the AAE system induces error, smaller errors are better. To treat such characteristics in AAE, CDDA determines between-class separability according to the class distance (i.e., difference in ages); two samples with similar ages are imposed to be close and those with spaced ages are imposed to be far apart. Furthermore, we propose an extension of CDDA called local CDDA (LCDDA), which aims at handling multimodality in samples. Experimental results revealed that CDDA and LCDDA could extract more discriminative features than FDA and LFDA.

An optimal selection criterion of the modulation and coding scheme (MCS) for maximizing spectral efficiency is proposed in consideration of the signaling overhead of mobile WiMAX systems with a hybrid automatic repeat request mechanism. A base station informs users about the resource assignments in each frame, and the allocation process generates a substantial signaling overhead, which influences the system throughput. However, the signaling overhead was ignored in previous MCS selection criteria. In this letter, the spectral efficiency is estimated on the basis of the signaling overhead and the number of transmissions. The performance of the proposed MCS selection criterion is evaluated in terms of the spectral efficiency in the mobile WiMAX system, with and without persistent allocation.

The development of the electricity market enables us to provide electricity of varied quality and price in order to fulfill power consumers' needs. Such customers choices should influence the process of adjusting power generation and spinning reserve, and, as a result, change the structure of a unit commitment optimization problem (UCP). To build a unit commitment model that considers customer choices, we employ fuzzy variables in this study to better characterize customer requirements and forecasted future power loads. To measure system reliability and determine the schedule of real power generation and spinning reserve, fuzzy Value-at-Risk (VaR) is utilized in building the model, which evaluates the peak values of power demands under given confidence levels. Based on the information obtained using fuzzy VaR, we proposed a heuristic algorithm called local convergence-averse binary particle swarm optimization (LCA-PSO) to solve the UCP. The proposed model and algorithm are used to analyze several test systems. Comparisons between the proposed algorithm and the conventional approaches show that the LCA-PSO performs better in finding the optimal solutions.

Brain-Computer Interfaces (BCIs) are systems that translate one's thoughts into commands to restore control and communication to severely paralyzed people, and they are also appealing to healthy people. One of the challenges is to improve the performance of BCIs, often measured by the accuracy and the trial duration, or the information transfer rate (ITR), i.e., the mutual information per unit time. Since BCIs are communications between a user and a system, error control schemes such as forward error correction and automatic repeat request (ARQ) can be applied to BCIs to improve the accuracy. This paper presents reliability-based ARQ (RB-ARQ), a variation of ARQ designed for BCIs, which employs the maximum posterior probability for the repeat decision. The current results show that RB-ARQ is more effective than the conventional methods, i.e., better accuracy when trial duration was the same, and shorter trial duration when the accuracy was the same. This resulted in a greater information transfer rate and a greater utility, which is a more practical performance measure in the P300 speller task. The results also show that such users who achieve a poor accuracy for some reason can benefit the most from RB-ARQ, which could make BCIs more universal.

Fair exchange is an important tool to achieve “fairness” of electronic commerce. Several previous schemes satisfy universally composable security which provides security preserving property under complex networks like the Internet. In recent years, as the demand for electronic commerce increases, fair exchange for electronic vouchers (e.g., electronic tickets, moneys, etc.) to obtain services or contents is in the spotlight. The definition of fairness for electronic vouchers is different from that for general electronic items (e.g., the sender must not do duplicate use of exchanged electronic vouchers). However, although there are universally composable schemes for electronic items, there is no previous study for electronic vouchers. In this paper, we introduce a universally composable definition of fair voucher exchange, that is, an ideal functionality of fair voucher exchange. Also, we prove the equivalence between our universally composable definition and the conventional definition for electronic vouchers. Thus, our formulation of the ideal functionality is justified. Finally, we propose a new fair voucher exchange scheme from non-blocking atomic commitment as black-box, which satisfies our security definition and is adequate for mobile environments. By instantiating general building blocks with known practical ones, our scheme can be also practical because it is implemented without trusted third party in usual executions.

We studied the interaction of Bis-diethylaminosilane (SiH2[N(C2H5)2]2, BDEAS) with a hydroxylized Si (001) surface for SiO2 thin-film growth using density functional theory (DFT). BDEAS was adsorbed on the Si surface and reacted with the H atom of hydroxyl (-OH) to produce the di-ethylaminosilane (-SiH2[N(C2H5)2], DEAS) group and di-ethylamine (NH(C2H5)2, DEA). Then, DEAS was able to react with another H atom of -OH to produce DEA and to form the O-(SiH2)-O bond at the inter-dimer, inter-row, or intra-dimer site. Among the three different sites, the intra-dimer site was the most probable when it came to forming the O-(SiH2)-O bond.

Let p be an odd prime number. We define a family of quaternary sequences of period 2p using generalized cyclotomic classes over the residue class ring modulo 2p. We compute exact values of the linear complexity, which are larger than half of the period. Such sequences are 'good' enough from the viewpoint of linear complexity.

For the Internet, system developers often have to estimate the QoS by simulation techniques or mathematical analysis. Probabilistic model checking can evaluate performance, dependability and stability of information processing systems with random behaviors. We apply a hybrid analysis approach onto real-time distributed systems. In the hybrid analysis approach, we perform stepwise analysis using probabilistic models of target systems in different abstract levels. First, we create a probabilistic model with detailed behavior of the system (called detailed model), and apply simulation on the detailed model. Next, based on the simulation results, we create a probabilistic model in an abstract level (called simplified model). Then, we verify qualitative properties using the probabilistic model checking techniques. This prevents from state-explosion. We evaluate the validity of our approach by comparing to simulation results of NS-2 using a case study of a video data streaming system. The experiments show that the result of the proposed approach is very close to that of NS-2 simulation. The result encourages the approach is useful for the performance analysis on various domain.

The number of Web applications handling online transaction is increasing, but verification of the correctness of Web application development has been done manually. This paper proposes a method for modeling, verifying and testing Web applications. In our method, a Web application is modeled using two finite-state automata, i.e., a page automaton which specifies Web page transitions, and an internal state automaton which specifies internal state transitions of the Web application. General properties for checking the Web application design are presented in LTL formulae and they are verified using the model checker Spin. Test cases examining the behavior of the Web application are also generated by utilizing the counterexamples obtained as the result of model checking. We applied our method to an example Web application to confirm its effectiveness.

Based on sliding-window rule application and extraction filtering, we present a framework for extracting multi-slot frames describing chemical reactions from Thai free text with unknown target-phrase boundaries. A supervised rule learning algorithm is employed for automatic construction of pattern-based extraction rules from hand-tagged training phrases. A filtering method is devised for removal of incorrect extraction results based on features observed from text portions appearing between adjacent slot fillers in source documents. Extracted reaction frames are represented as concept expressions in description logics and are used as metadata for document indexing. A document knowledge base supporting semantics-based information retrieval is constructed by integrating document metadata with domain-specific ontologies.

In this letter, we give a generalized construction for sets of frequency-hopping sequences (FHSs) based on power-residue sequences. Our construction encompasses a known optimal construction and can generate new optimal sets of FHSs which simultaneously achieve the Peng-Fan bound and the Lempel-Greenberger bound.

This survey summarizes the state-of-the-art research on network coding, mainly focusing on its applications to computer networking. Network coding generalizes traditional store-and-forward routing techniques by allowing intermediate nodes in networks to encode several received packets into a single coded packet before forwarding. Network coding was proposed in 2000, and since then, it has been studied extensively in the field of computer networking. In this survey, we first summarize linear network coding and provide a taxonomy of network coding research, i.e., the network coding design problem and network coding applications. Moreover, the latter is subdivided into throughput/capacity enhancement, robustness enhancement, network tomography, and security. We then discuss the fundamental characteristics of network coding and diverse applications of network coding in details, following the above taxonomy.