Safety critical systems are often modeled using Time Petri Nets (TPN) for analyzing their reliability with formal verification methods. This paper proposed an efficient verification method for TPN introducing bounded model checking based on satisfiability solving. The proposed method expresses time constraints of TPN by Difference Logic (DL) and uses SMT solvers for verification. Its effectiveness was also demonstrated with an experiment.

This letter presents a novel technique to achieve a fast inference of the binarized convolutional neural networks (BCNN). The proposed technique modifies the structure of the constituent blocks of the BCNN model so that the input elements for the max-pooling operation are binary. In this structure, if any of the input elements is +1, the result of the pooling can be produced immediately; the proposed technique eliminates such computations that are involved to obtain the remaining input elements, so as to reduce the inference time effectively. The proposed technique reduces the inference time by up to 34.11%, while maintaining the classification accuracy.

We propose a non-photorealistic rendering method for generating edge-preserving bubble images from gray-scale photographic images. Bubble images are non-photorealistic images embedded in many bubbles, and edge-preserving bubble images are bubble images where edges in photographic images are preserved. The proposed method is executed by an iterative processing using absolute difference in window. The proposed method has features that processing is simple and fast. To validate the effectiveness of the proposed method, experiments using various photographic images are conducted. Results show that the proposed method can generate edge-preserving bubble images by preserving the edges of photographic images and the processing speed is high.

This paper presents new encoding and decoding methods for Berlekamp-Preparata convolutional codes (BPCCs) based on tail-biting technique. The proposed scheme can correct a single block of n bit errors relative to a guard space of m error-free blocks while no fractional rate loss is incurred. The proposed tail-biting BPCCs (TBBPCCs) can attain optimal complete burst error correction bound. Therefore, they have the optimal phased-burst-error-correcting capability for convolutional codes. Compared with the previous scheme, the proposed scheme can also improve error correcting capability.

In this paper, we propose an image to sound mapping method. This technique treats an image as a spectrogram and maps it to a sound by taking inverse FFT of the spectrogram. Amplitude spectra of a speech signal are embedded to the spectrogram to give speech intelligibility for the mapped sound. Specifically, we hold amplitude spectra of a speech signal with strong power and embed the image brightness in other frequency bands. Holding amplitude spectra of a speech signal with strong power preserves a speech spectral envelope and improves the speech quality of the mapped sound. The amplitude spectra of the mapped sound with weak power represent the image brightness, and then the image is successfully reconstructed from the mapped sound. Simulation results show that the proposed method achieves sufficient speech quality.

To estimate angle, velocity, and range information of multiple targets jointly in FMCW MIMO radar, two-dimensional (2D) MUSIC with matched filtering and FFT algorithm is proposed. By reformulating the received FMCW signal of the colocated MIMO radar, we exploit 2D MUSIC to estimate the angle and Doppler frequency of multiple targets. Then by using a matched filter together with the estimated angle and Doppler frequency and FFT operation, the range of the target is estimated. To effectively estimate the parameters of multiple targets with large distance differences, we also propose a successive interference cancellation method that uses the orthogonal projection. That is, rather than estimating the multiple target parameters simultaneously using 2D MUSIC, we estimate the target parameters sequentially, in which the parameters of the target having strongest reflected power are estimated first and then, their effect on the received signal is canceled out by using the orthogonal projection. Simulations verify the performance of the proposed algorithm.

Recent years have witnessed a rapid increase in cyber-attacks through unauthorized accesses and DDoS attacks. Since packet classification is a fundamental technique to prevent such illegal communications, it has gained considerable attention. Packet classification is achieved with a linear search on a classification rule list that represents the packet classification policy. As such, a large number of rules can result in serious communication latency. To decrease this latency, the problem is formalized as optimal rule ordering (ORO). In most cases, this problem aims to find the order of rules that minimizes latency while satisfying the dependency relation of the rules, where rules ri and rj are dependent if there is a packet that matches both ri and rj and their actions applied to packets are different. However, there is a case in which although the ordering violates the dependency relation, the ordering satisfies the packet classification policy. Since such an ordering can decrease the latency compared to an ordering under the constraint of the dependency relation, we have introduced a new model, called relaxed optimal rule ordering (RORO). In general, it is difficult to determine whether an ordering satisfies the classification policy, even when it violates the dependency relation, because this problem contains unsatisfiability. However, using a zero-suppressed binary decision diagram (ZDD), we can determine it in a reasonable amount of time. In this paper, we present a simulated annealing method for RORO which interchanges rules by determining whether rules ri and rj can be interchanged in terms of policy violation using the ZDD. The experimental results show that our method decreases latency more than other heuristics.

This paper proposes a generative moment matching network (GMMN)-based post-filtering method for providing inter-utterance pitch variation to singing voices and discusses its application to our developed mixing method called neural double-tracking (NDT). When a human singer sings and records the same song twice, there is a difference between the two recordings. The difference, which is called inter-utterance variation, enriches the performer's musical expression and the audience's experience. For example, it makes every concert special because it never recurs in exactly the same manner. Inter-utterance variation enables a mixing method called double-tracking (DT). With DT, the same phrase is recorded twice, then the two recordings are mixed to give richness to singing voices. However, in synthesized singing voices, which are commonly used to create music, there is no inter-utterance variation because the synthesis process is deterministic. There is also no inter-utterance variation when only one voice is recorded. Although there is a signal processing-based method called artificial DT (ADT) to layer singing voices, the signal processing results in unnatural sound artifacts. To solve these problems, we propose a post-filtering method for randomly modulating synthesized or natural singing voices as if the singer sang again. The post-filter built with our method models the inter-utterance pitch variation of human singing voices using a conditional GMMN. Evaluation results indicate that 1) the proposed method provides perceptible and natural inter-utterance variation to synthesized singing voices and that 2) our NDT exhibits higher double-trackedness than ADT when applied to both synthesized and natural singing voices.

A convolutional neural network (CNN) for broadband direction of arrival (DOA) estimation of far-field electromagnetic signals is presented. The proposed algorithm performs a nonlinear inverse mapping from received signal to angle of arrival. The signal model used for algorithm is based on the circular antenna array geometry, and the phase component extracted from the spatial covariance matrix is used as the input of the CNN network. A CNN model including three convolutional layers is then established to approximate the nonlinear mapping. The performance of the CNN model is evaluated in a noisy environment for various values of signal-to-noise ratio (SNR). The results demonstrate that the proposed CNN model with the phase component of the spatial covariance matrix as the input is able to achieve fast and accurate broadband DOA estimation and attains perfect performance at lower SNR values.

Skip Graph is a promising distributed data structure for large scale systems and known for its capability of range queries. Although several methods of routing range queries in Skip Graph have been proposed, they have inefficiencies such as a long path length or a large number of messages. In this paper, we propose a novel routing method for range queries named Split-Forward Broadcasting (SFB). SFB introduces a divide-and-conquer approach, enabling nodes to make full use of their routing tables to forward a range query. It brings about a shorter average path length than existing methods, as well as a smaller number of messages by avoiding duplicate transmission. We clarify the characteristics and effectiveness of SFB through both analytical and experimental comparisons. The results show that SFB can reduce the average path length roughly 30% or more compared with a state-of-the-art method.

In this paper, we describe a novel low-delay 4K 120-fps real-time HEVC decoder with a parallel processing architecture that conforms to the HEVC main 4:2:2 10 profile. It supports the hierarchical temporal scalable streams required for Ultra High Definition high-frame-rate broadcasting and also supports low-delay and high-bitrate decoding for video transmission uses. To achieve this support, the decoding processes are parallelized and pipelined at the frame level, slice level, and coding tree unit row level. The proposed decoder was implemented on three FPGAs operated at 133 and 150 MHz, and it achieved 300-Mbps stream decoding and 37-msec end-to-end delay with our concurrently developed 4K 120-fps encoder.

Heterogeneous networks (HetNets) technology is expected to be applied in next generation cellular networks to boost system capacity. However, applying HetNets introduces a significant amount of interference among different tiers within the same cell. In this paper, we propose a weighted rank constrained rank minimization (WRCRM) based interference alignment (IA) approach for three-tier HetNets. The concept of RCRM is applied in a different way to deal with the basic characteristic of different tiers: their different interference tolerance. In the proposed WRCRM approach, interference components at different tiers are weighted with different weighting factors (WFs) to reflect their vulnerability to interference. First, we derive an inner and a loose outer bound on the achievable degrees of freedom (DoF) for the three-tier system that is modeled as a three-user mutually interfering broadcast channel (MIBC). Then, the derived bounds along with the well-known IA feasibility conditions are used to show the effectiveness of the proposed WRCRM approach. Results show that there exist WF values that maximize the achievable interference-free dimensions. Moreover, adjusting the required number of DoF according to the derived bounds improves the performance of the WRCRM approach.

A context-aware system always needs to adapt its behaviors according to context changes; therefore, modeling context-aware requirements is a complex task. With the increasing use of mobile computing, research on methods of modeling context-aware requirements have become increasingly important, and a large number of relevant studies have been conducted. However, no comprehensive analysis of the challenges and achievements has been performed. The methodology of systematic literature review was used in this survey, in which 68 reports were selected as primary studies. The challenges and methods to confront these challenges in context-aware requirement modeling are summarized. The main contributions of this work are: (1) four challenges and nine sub-challenges are identified; (2) eight kinds of methods in three categories are identified to address these challenges; (3) the extent to which these challenges have been solved is evaluated; and (4) directions for future research are elaborated.

The objective of this letter is to present a family of q-ary codes with parameters $[rac{q^m-1}{q-1},rac{q^m-1}{q-1}-2m,d]$, where m is a positive integer, q is a power of an odd prime and 4≤d≤5. The parameters are proved to be optimal or almost optimal with respect to an upper bound on linear codes.

Utilization of local memory from real-time embedded systems to high performance systems with multi-core processors has become an important factor for satisfying hard deadline constraints. However, challenges lie in the area of efficiently managing the memory hierarchy, such as decomposing large data into small blocks to fit onto local memory and transferring blocks for reuse and replacement. To address this issue, this paper presents a compiler optimization method that automatically manage local memory of multi-core processors. The method selects and maps multi-dimensional data onto software specified memory blocks called Adjustable Blocks. These blocks are hierarchically divisible with varying sizes defined by the features of the input application. Moreover, the method introduces mapping structures called Template Arrays to maintain the indices of the decomposed multi-dimensional data. The proposed work is implemented on the OSCAR automatic parallelizing compiler and evaluations were performed on the Renesas RP2 8-core processor. Experimental results from NAS Parallel Benchmark, SPEC benchmark, and multimedia applications show the effectiveness of the method, obtaining maximum speed-ups of 20.44 with 8 cores utilizing local memory from single core sequential versions that use off-chip memory.

The equivalent transmission-path model is a propagation-oriented channel model for predicting the bit error rate due to intersymbol interference in single-input single-output systems. We extend this model to develop a new calculation scheme for maximal-ratio combining diversity reception in single-input multiple-output configurations. A key part of the study is to derive a general formula expressing the joint probability density function of the amplitude ratio and phase difference of the two-path model. In this derivation, we mainly take a theoretical approach with the aid of Monte Carlo simulation. Then, very high-accuracy estimation of the average bit error rate due to intersymbol interference (ISI) for CQPSK calculated based on the model is confirmed by computer simulation. Finally, we propose a very simple calculation formula for the prediction of the BER due to ISI that is commonly applicable to various modulation/demodulation schemes, such as CQPSK, DQPSK, 16QAM, and CBPSK in maximal-ratio combining diversity reception.

Differential code biases (DCBs) are important parameters that must be estimated accurately for precise positioning and Satellite Based Augmentation Systems (SBAS) ionospheric related parameter generation. In this paper, in order to solve the performance degradation problem of the traditional minimum STD searching algorithm in disturbed ionosphere status and in geomagnetic low latitudes, we propose a linear planar based minimum STD searching algorithm. Firstly, we demonstrate the linear planar trend of the local vertical TEC and introduce the linear planar model based minimum standard variance searching method. Secondly, we validate the correctness of our proposed method through theoretical analysis and propose bias detection to avoid large estimation bias. At last, we show the performance of our proposed method under different geomagnetic latitudes, different seasons and different ionosphere status. The experimental results show that for the traditional minimum STD searching algorithm based on constant model, latitude difference is the key factor affecting the performance of DCB estimation. The DCB estimation performance in geomagnetic mid latitudes is the best, followed by the high latitudes and the worst is for the low latitudes. While the algorithm proposed in this paper can effectively solve the performance degradation problem of DCB estimation in geomagnetic low latitudes by using the linear planar model which is with a higher degree of freedom to model the local ionosphere characteristics and design dJ to screen the epochs. Through the analysis of the DCB estimation results of a large number of stations, it can be found that the probability of large estimation deviation of the traditional method will increase obviously under the disturb ionosphere conditions, but the algorithm we proposed can effectively control the amplitude of the maximum deviation and alleviate the probability of large estimation deviation in disturb ionosphere status.

This letter proposes a new superpixel segmentation algorithm based on global similarity and contour region transformation. The basic idea is that pixels surrounded by the same contour are more likely to belong to the same object region, which could be easily clustered into the same superpixel. To this end, we use contour scanning to estimate the global similarity between pixels and corresponded centers. In addition, we introduce pixel's gradient information of contour transform map to enhance the pixel's global similarity to overcome the missing contours in blurred region. Benefited from our global similarity, the proposed method could adherent with blurred and low contrast boundaries. A large number of experiments on BSDS500 and VOC2012 datasets show that the proposed algorithm performs better than traditional SLIC.

Music classification has been inspired by the remarkable success of deep learning. To enhance efficiency and ensure high performance at the same time, a hybrid architecture that combines deep learning and Broad Learning (BL) is proposed for music classification tasks. At the feature extraction stage, the Random CNN (RCNN) is adopted to analyze the Mel-spectrogram of the input music sound. Compared with conventional CNN, RCNN has more flexible structure to adapt to the variance contained in different types of music. At the prediction stage, the BL technique is introduced to enhance the prediction accuracy and reduce the training time as well. Experimental results on three benchmark datasets (GTZAN, Ballroom, and Emotion) demonstrate that: i) The proposed scheme achieves higher classification accuracy than the deep learning based one, which combines CNN and LSTM, on all three benchmark datasets. ii) Both RCNN and BL contribute to the performance improvement of the proposed scheme. iii) The introduction of BL also helps to enhance the prediction efficiency of the proposed scheme.

Many countries have deregulated their electricity retail markets to offer lower electricity charges to consumers. However, many consumers have not switched their suppliers after the deregulation, and electricity suppliers do not tend to reduce their charges intensely. This paper proposes an electricity market model and evolutionary game to analyze the behavior of consumers in electricity retail markets. Our model focuses on switching costs such as an effort at switching, costs in searching for other alternatives, and so on. The evolutionary game examines whether consumers choose a strategy involving exploration of new alternatives with the searching costs as “cooperators” or not. Simulation results demonstrate that the share of cooperators was not improved by simply giving rewards for cooperators as compensation for searching costs. Furthermore, the results also suggest that the degree of cooperators in a network among consumers has a vital role in increasing the share of cooperators and switching rate.