Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.

Recent development in network technology can realize the control of a remote plant by a digital controller. However, there is a delay caused by data transmission of control inputs and outputs. The delay degrades the control performance without taking it into consideration. In general, it is a difficult problem to identify the delay beforehand. We also assume that the plant's parameters have uncertainty. To solve the problem, we use reinforcement learning to achieve optimal digital control. First, we consider state feedback control. Next, we consider the case where the plant's outputs are observed, and apply reinforcement learning to output feedback control. Finally, we demonstrate by simulation that the proposed control method can search for the optimal gain and that it can adapt to the change of the delay.

In previous papers by the authors, a new scheme for diagnosis of stochastic discrete event systems, called sequence profiling (SP), is proposed. From given event logs, N-gram models that approximate the behavior of the target system are extracted. N-gram models are used for discovering discrepancy between observed event logs and the behavior of the system in the normal situation. However, when the target system is a distributed system consisting of several subsystems, event sequences from subsystems may be interleaved, and SP cannot separate the faulty event sequence from the interleaved sequence. In this paper, we introduce wildcard characters into event patterns. This contributes to removing the effect by subsystems which may not be related to faults.

Event-triggered and self-triggered control methods are an important control strategy in networked control systems. Event-triggered control is a method that the measured signal is sent to the controller (i.e., the control input is recomputed) only when a certain condition is satisfied. Self-triggered control is a method that the control input and the (non-uniform) sampling interval are computed simultaneously. In this paper, we propose new methods of event-triggered control and self-triggered control from the viewpoint of online optimization (i.e., model predictive control). In self-triggered control, the control input and the sampling interval are obtained by solving a pair of a quadratic programming (QP) problem and a mixed integer linear programming (MILP) problem. In event-triggered control, whether the control input is updated or not is determined by solving two QP problems. The effectiveness of the proposed methods is presented by numerical examples.

In this paper, we formulate an optimal stabilization problem of quantitative discrete event systems (DESs) under partial observation. A DES under partial observation is a system where its behaviors cannot be completely observed by a supervisor. In our framework, the supervisor observes not only masked events but also masked states. Our problem is then to synthesize a supervisor that drives the DES to a given target state with the minimum cost based on the detected sequences of masked events and states. We propose an algorithm for deciding the existence of an optimal stabilizing supervisor, and compute it if it exists.

We consider a bisimilarity control problem for transition systems. For this control problem, a necessary and sufficient condition for its solvability and a method for synthesizing a state feedback controller have been presented in the literature. However, the state of the system to be controlled is not necessarily observable. In this paper, we synthesize an observer-based output feedback controller for the bisimilarity control problem under a certain condition, and show that this output feedback controller is a solution to the control problem.

Analysis of security governed by dynamics of power systems, which we refer to as dynamic security analysis, is a primary but challenging task because of its hybrid nature, that is, nonlinear continuous-time dynamics integrated with discrete switchings. In this paper, we formulate this analysis problem as checking the reachability of a mathematical model representing dynamic performances of a target power system. We then propose a computational approach to the analysis based on the so-called RRT (Rapidly-exploring Random Tree) algorithm. This algorithm searches for a feasible trajectory connecting an initial state possibly at a lower security level and a target set with a desirable higher security level. One advantage of the proposed approach is that it derives a concrete control strategy to guarantee the desirable security level if the feasible trajectory is found. The performance and effectiveness of the proposed approach are demonstrated by applying it to two running examples on power system studies: single machine-infinite system and two-area system for frequency control problem.

Workflow nets (WF-nets for short) are a mathematical model of real world workflows. A WF-net is often updated in accordance with the change of real world. This may cause places that are redundant from the viewpoint of the behavior. Such places are called implicit. We first proposed a necessary and sufficient condition to find implicit places. Then we proved that removing of implicit places is a reduction operation which forms branching bisimilarity. We also constructed an algorithm for the reduction. Next, we applied the proposed reduction operation to WF-net refactoring. Then we showed the usefulness of the proposed refactoring with two examples.

Many actual systems, e.g. computer programs, can be modeled as a subclass of Petri nets, called bridge-less workflow nets. For bridge-less workflow nets, we revealed the following properties: (i) any acyclic bridge-less workflow net is free choice; (ii) an acyclic bridge-less workflow net is sound iff it is well-structured; and (iii) any sound bridge-less workflow net is well-structured. We also proposed a necessary and sufficient condition to decide whether a given workflow net is bridge-less, and then constructed a polynomial-time procedure for it.

Analog and digital collaborative design techniques for wireless SoCs are reviewed in this paper. In wireless SoCs, delicate analog performance such as sensitivity of the receiver is easily degraded due to interferences from digital circuit blocks. On the other hand, an analog performance such as distortion is strongly compensated by digital assist techniques with low power consumption. In this paper, a sensitivity recovery technique using the analog and digital collaborative design, and digital assist techniques to achieve low-power and high-performance analog circuits are presented. Such analog and digital collaborative design is indispensable for wireless SoCs.

To achieve low-voltage low-power SRAMs, two proposals are demonstrated. One is a multi-power-supply five-transistor cell (5T cell), assisted by a boosted word-line voltage and a mid-point sensing enabled by precharging bit-lines to V_DD/2. The cell enables to reduce V_DD to 0.5V or less for a given speed, or enhance speed for a given V_DD. The other is a partial activation of a compact multi-divided open-bit-line array for low power. Layout and post-layout simulation with a 28-nm fully-depleted planar-logic SOI MOSFET reveal that a 0.5-V 5T-cell 4-kb array in a 128-kb SRAM core using the proposals is able to achieve x2-3 faster cycle time and x11 lower power than the counterpart 6T-cell array, suggesting a possibility of a 730-ps cycle time at 0.5V.

Patch clamp measurement technique is one of the most important techniques in the field of electrophysiology. The elucidation of the channels, nerve cells, and brain activities as well as contribution of the treatment of neurological disorders is expected from the measurement of ion current. A current-to-voltage converter, which is the front end circuit of the patch clamp measurement system is fabricated using 0.18µm CMOS technology. The current-to-voltage converter requires a resistance as high as 50MΩ as a feedback resistor in order to ensure a high signal-to-noise ratio for very small signals. However, the circuit becomes unstable due to the large parasitic capacitance between the poly layer and the substrate of the on-chip feedback resistor and the instability causes the peaking at lower frequency. The instability of a current-to-voltage converter with a high-resistance as a feedback resistor is analyzed theoretically. A compensation circuit to stabilize the amplifier by driving the N-well under poly resistor to suppress the effect of parasitic capacitance using buffer circuits is proposed. The performance of the proposed circuit is confirmed by both simulation and measurement of fabricated chip. The peaking in frequency characteristic is suppressed properly by the proposed method. Furthermore, the bandwidth of the amplifier is expanded up to 11.3kHz, which is desirable for a patch clamp measurement. In addition, the input referred rms noise with the range of 10Hz ∼ 10kHz is 2.09 A_rms and is sufficiently reach the requirement for measure of both whole-cell and a part of single-channel recordings.

Noise and area consumption has been a trade-off in circuit design. Especially for switched-capacitor filters (SCF), kT/C noise gives a limitation to the minimum value of unit capacitance. In case of SCFs with a large capacitance spread, this limitation will result in a large area consumption due to large capacitors. This paper introduces a technique to reduce capacitance spread using charge scaling. It will be shown that this technique can reduce total capacitance of SCFs without deteriorating their noise performances. A design method to reduce the output noise of SC low-pass filters (LPF) based on the combination of cut-set scaling, charge scaling and adaptive configuration is proposed. The proposed technique can reduce the output noise voltage by 30% for small input signals.

A new gain enhancement technique for an operational amplifier (opamp) using a replica amplifier is presented to reduce a sensitivity of a gain mismatch between the main amplifier and the replica amplifier which limits a gain-enhancement factor in the conventional replica-amp techniques. In the proposed technique, the replica amplifier is used to only amplify an error voltage of the main amplifier. The outputs of the main amplifier and the replica amplifier are added to cancel the error voltage of the main amplifier. The proposed technique can also achieve a higher output voltage swing because the replica amplifier amplifies only the error voltage. In case of using a fully-differential common-source opamp for the main amplifier and a telescopic opamp for the replica amplifier, Monte Carlo simulation at 100 iterations shows that the proposed amplifier has almost the same gain variation with 15.5dB gain enhancement and about five times output voltage swing expanding for a supply voltage of 1.2V compared with the single closed-loop amplifier using the telescopic opamp.

This letter presents a new time-digital single-slope ADC (TDSS) architecture for CMOS image sensors. In the proposed ADC, a conventional single-slope ADC is used in coarse phase and a time to digital convertor is employed in fine phase. Through second comparison of the two different slope voltages (discharge input voltage and ramp voltage), the proposed ADC achieves low bit precision compensation. Compared with multiple-ramp single-slope (MRSS) ADC, the proposed ADC not only has a simple digital judgment circuit, but also increases conversion speed without complicated structure of ramp generator. A 10-bit TDSS ADC consisting of 7-bit conventional single-slope ADC and 3-bit time to digital converter was realized in a 0.13µm CIS process. Simulations demonstrate that the conversion speed of a TDSS ADC is almost 3.5 times faster than that of a single-slope ADC.

This paper proposes a method based on modulation transfer function (MTF) to restore the power envelope of noisy reverberant speech by using a Kalman filter with linear prediction (LP). Its advantage is that it can simultaneously suppress the effects of noise and reverberation by restoring the smeared MTF without measuring room impulse responses. This scheme has two processes: power envelope subtraction and power envelope inverse filtering. In the subtraction process, the statistical properties of observation noise and driving noise for power envelope are investigated for the criteria of the Kalman filter which requires noise to be white and Gaussian. Furthermore, LP coefficients drastically affect the Kalman filter performance, and a method is developed for deriving LP coefficients from noisy reverberant speech. In the dereverberation process, an inverse filtering method is applied to remove the effects of reverberation. Objective experiments were conducted under various noisy reverberant conditions to evaluate how well the proposed Kalman filtering method based on MTF improves the signal-to-error ratio (SER) and correlation between restored power envelopes compared with conventional methods. Results showed that the proposed Kalman filtering method based on MTF can improve SER and correlation more than conventional methods.

Different from application-specific digital microfluidic biochips, a general-purpose design has several advantages such as dynamic reconfigurability, and fast on-line evaluation for real-time applications. To achieve such superiority, this design typically activates each electrode in the chip using an individual control pin. However, as the design complexity increases substantially, an order-of-magnitude increase in the number of control pins will significantly affect the manufacturing cost. To tackle this problem, several methods adopting a pin-sharing mechanism for general-purpose designs have been proposed. Nevertheless, these approaches sacrifice the flexibility of droplet movement, and result in an increase of bioassay completion time. In this paper, we present a novel pin-count reduction design methodology for general-purpose microfluidic biochips. Distinguished from previous approaches, the proposed methodology not only reduces the number of control pins significantly but also guarantees the full flexibility of droplet movement to ensure the minimal bioassay completion time.

A multisignature (MS) scheme enables a group of signers to produce a compact signature on a common message. In analyzing security of MS schemes, a key registration protocol with proof-of-possession (POP) is considered to prevent rogue key attacks. In this paper, we refine the POP-based security model by formalizing a new strengthened POP model and showing relations between the previous POP models and the new one. We next suggest a MS scheme that achieves: (1) non-interactive signing process, (2) O(1) pairing computations in verification, (3) tight security reduction under the co-CDH assumption, and (4) security under the new strengthened POP model. Compared to the tightly-secure BNN-MS scheme, the verification in ours can be at least 7 times faster at the 80-bit security level and 10 times faster at the 128-bit security level. To achieve our goal, we introduce a novel and simple POP generation method that can be viewed as a one-time signature without random oracles. Our POP technique can also be applied to the LOSSW-MS scheme (without random oracles), giving the security in the strengthened POP model.

In a public-key encryption scheme, if a sender is not concerned about the security of a message and is unwilling to generate costly randomness, the security of the encrypted message can be compromised. In this work, we characterize such lazy parties, who are regarded as honest parties, but are unwilling to perform a costly task when they are not concerned about the security. Specifically, we consider a rather simple setting in which the costly task is to generate randomness used in algorithms, and parties can choose either perfect randomness or a fixed string. We model lazy parties as rational players who behave rationally to maximize their utilities, and define a security game between the parties and an adversary. Since a standard secure encryption scheme does not work in this setting, we provide constructions of secure encryption schemes in various settings.

This paper gives an array-based practical encoder for the lossless data compression algorithm known as Compression by Substring Enumeration (CSE). The encoder makes use of the relation between CSE and the Burrows-Wheeler transform. We also modify the decoding algorithm to accommodate to the proposed encoder. Thanks to the proposed encoder and decoder, we can apply CSE to long data of more than tens of megabytes. We show compression results obtained when we perform experiments on such long data. The results empirically validate theoretical predictions on CSE.

In this paper, we propose an example-based single image super resolution (SR) method by l₂ approximation with self-sampled image patches. Example-based super resolution methods can reconstruct high resolution image patches by a linear combination of atoms in an overcomplete dictionary. This reconstruction requires a pair of two dictionaries created by tremendous low and high resolution image pairs from the prepared image databases. In our method, we introduce the dictionary by random sampling patches from just an input image and eliminate its training process. This dictionary exploits the self-similarity of images and it will no more depend on external image sets, which consern the storage space or the accuracy of referred image sets. In addition, we modified the approximation of input image to an l₂-norm minimization problem, instead of commonly used sparse approximation such as l₁-norm regularization. The l₂ approximation has an advantage of computational cost by only solving an inverse problem. Through some experiments, the proposed method drastically reduces the computational time for the SR, and it provides a comparable performance to the conventional example-based SR methods with an l₁ approximation and dictionary training.

This paper proposes a novel technology to detect the orientation of an image relying on its contour which is noised to varying degrees. For the image orientation detection, most methods regard to the landscape image and the image taken of a single object. In these cases, the contours of these images are supposed to be immune to the noise. This paper focuses on the the contour noised after image segmentation. A polar orientation descriptor Orientation Context is viewed as a feature to describe the coarse distribution of the contour points. This descriptor is verified to be independent of translation, isotropic scaling, and rotation transformation by theory and experiment. The relative orientation depends on the minimum distance Roulette Distance between the descriptor of a template image and that of a test image. The proposed method is capable of detecting the direction on the interval from 0 to 359 degrees which is wider than the former contour-based means (Distance Phase [1], from 0 to 179 degrees). What's more, the results of experiments show that not only the normal binary image (Noise-0, Accuracy-1: 84.8%) (defined later) achieves more accurate orientation but also the binary image with slight contour noise (Noise-1, Accuracy-1: 73.5%) could obtain more precise orientation compared to Distance Phase (Noise-0, Accuracy-1: 56.3%; Noise-1, Accuracy-1: 27.5%). Although the proposed method (O(op²)) takes more time to detect the orientation than Distance Phase (O(st)), it could be realized including the preprocessing in real time test with a frame rate of 30.

The new generation video standard, i.e., High-efficiency Video Coding (HEVC), shows a significantly improved efficiency relative to the last standard, i.e., H.264. However, the quad tree structured coding units (CUs), which are adopted in HEVC to improve compression efficiency, cause high computational complexity. In this study, a novel fast algorithm is proposed for CU partition in intra coding to reduce the computational complexity. A rough minimum depth prediction of the largest CU method and an early termination method for CU partition based on the total coding bits of the current CU are employed. Many approaches have been proposed to reduce the encoding complexity of HEVC, but these methods do not use the total coding bits of the current CU as the main basis for judgment to judge the CU complexity. Compared with the reference software HM16.6, the proposed algorithm reduces encoding time by 45% on average and achieves an approximately 1.1% increase in Bjntegaard delta bit rate and a negligible peak signal-to-noise ratio loss.

In this paper, an iterative optimal method is proposed to design the prototype filters for a fast filter bank (FFB) with low complexity, aiming to control the optimum ripple magnitude tolerance of each filter according to the overall specifications. This problem is formulated as an optimization problem for which the total number of multiplications is to be minimized subject to the constrained ripple in the passband and stopband. In the following, an iterative solution is proposed to solve this optimization problem for the purpose of obtaining the impulse response coefficients with low complexity at each stage. Simulations are conducted to verify the performance of the proposed scheme and show that compared with the original method, the proposed scheme can reduce about 24.24% of multiplications. In addition, the proposed scheme and the original method provide similar mean square error (MSE) and the mean absolute error (MAE) of the frequency response.

This paper presents a novel MEMD interval thresholding denoising, where relevant modes are selected by the similarity measure between the probability density functions of the input and that of each mode. Simulation and measured EEG data processing results show that the proposed scheme achieves better performance than other traditional denoisings.

This paper studies the problem of recovering an arbitrarily distributed sparse matrix from its one-bit (1-bit) compressive measurements. We propose a matrix sketching based binary method iterative hard thresholding (MSBIHT) algorithm by combining the two dimensional version of BIHT (2DBIHT) and the matrix sketching method, to solve the sparse matrix recovery problem in matrix form. In contrast to traditional one-dimensional BIHT (BIHT), the proposed algorithm can reduce computational complexity. Besides, the MSBIHT can also improve the recovery performance comparing to the 2DBIHT method. A brief theoretical analysis and numerical experiments show the proposed algorithm outperforms traditional ones.

The feasibility condition of interference alignment (IA) for multiple-input multiple-output two-way interference channel is studied in this paper. A necessary condition and a sufficient condition on the IA feasibility are established and the sum degrees of freedom (DoF) for a broad class of network topologies is characterized. The numerical results demonstrate that two-way operation with appropriate IA is able to achieve larger sum DoF than the conventional one-way operation.

Nowadays, the batteryless sensor system is widely used for Internet of things (IoT) system. Especially, batteryless backscatter system has a great significance in that it permits us to communicate without power supply devices. However, conventional backscatter system requires high power reader and this can be a problem with the communication efficiency. Therefore, this letter proposes a new transmission scheme on the batteryless backscatter system in order to solve this problem. In the proposed scheme, the mobile devices which embed Wi-Fi chipset are used as a reader. The tag obtains Internet connectivity from the reader. Since the tag can not decode the general Wi-Fi packet, new algorithm of the scheme uses a specially designed packet. In this letter, the designing method for the decodable packet is proposed. Moreover, the scheme implements beamforming to improve the reliability. By concentrating the power to the designated direction, the robust communication can be achieved. The simulation results show that the proposed scheme offers reliable Internet connectivity without extra battery.

Recently, H. Liu et al. [H. Liu, M. Liang, and H. Sun, A secure and efficient certificateless aggregate signature scheme, IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences, vol.E97-A, no.4, pp.991-915, 2014] proposed a new certificateless aggregate signature (CLAS) scheme and demonstrated that it was provably secure in the random oracle model. However, in this letter, we show that their scheme cannot provide unforgeability, i.e., an adversary having neither the user's secret value nor his/her partial private key can forge a legal signature of any message.

To overcome the privacy limitations of conventional PKI (Public Key Infrastructure) systems, combinatorial certificate schemes assign each certificate to multiple users so that users can perform anonymous authentication. From a certificate pool of N certificates, each user is given n certificates. If a misbehaving user revokes a certificate, all the other users who share the revoked certificate will also not be able to use it. When an honest user shares a certificate with a misbehaving user and the certificate is revoked by the misbehaving user, the certificate of the honest user is said to be covered. To date, only the analysis for the worst scenario has been conducted; the probability that all n certificates of an honest user are covered when m misbehaving users revoke their certificates is known. The subject of this article is the following question: how many certificates (among n certificates) of an honest user are covered on average when m misbehaving users revoke their certificates? We present the first average-case analysis of the cover probability in combinatorial certificate schemes.

Pseudorandom binary sequences balanced and with optimal autocorrelation have many applications in the stream cipher, communication, coding theory, etc. Constructing a binary sequences with three-level autocorrelation is equivalent to finding the corresponding characteristic set of the sequences that should be an almost difference set. In the work of T.W. Cusick, C. Ding, and A. Renvall in 1998, the authors gave the necessary and sufficient conditions by which a set of octic residues modulo an odd prime forms an almost difference set. In this paper we show that no integers verify those conditions by the theory of generalized Pell equations. In addition, by relaxing the definition of almost difference set given by the same authors, we could construct two classes of modified almost difference sets and two ones of difference sets from the set of octic residues.

In this letter, a new method is presented to suppress fractional pseudocodewords by eliminating small instantons of irregular low-density parity-check (LDPC) codes under the linear programming (LP) decoding over the binary symmetric channel (BSC). By appending several new rows found by the integer linear programming formulation to the original parity-check matrix, the optimal distribution spectrum of BSC-instantons in the modified code is obtained. Simulation results show that the proposed method can improve the fractional distance of parity-check matrices and considerably enhance the error-correcting performance of irregular LDPC codes under the LP decoding at the cost of a slightly loss of the original code rate.

The acquisition of accurate channel state information at the transmitter (CSIT) is a difficult task in multiple-input multiple-output (MIMO) systems. Partial CSIT is a more realistic assumption, especially for high-mobility mobile users (MUs) whose channel varies very rapidly. In this letter, we propose a MIMO two-way relaying (MTWR) scheme, in which the communication between the BS and a high-mobility MU is assisted by other low-mobility MUs serving as relays. This produces a beamforming effect that can significantly improve the performance of the high-mobility MU, especially for a large number of MUs and unreliable CSIT.