Petri net is a powerful modeling tool for concurrent systems. Liveness, which is a problem to verify there exists no local deadlock, is one of the most important properties of Petri net to analyze. Computational complexity of liveness of a general Petri net is deterministic exponential space. Liveness is studied for subclasses of Petri nets to obtain necessary and sufficient conditions that need less computational cost. These are mainly done using a subset of places called siphons. CS-property, which denotes that every siphon has token(s) in every reachable marking, in one of key properties in liveness analysis. On the other hand, normal Petri net is a subclass of Petri net whose reachability set can be effectively calculated. This paper studies computational complexity of liveness problem of normal Petri nets. First, it is shown that liveness of a normal Petri net is equivalent to cs-property. Then we show this problem is co-NP complete by deriving a nondeterministic algorithm for non-liveness which is similar to the algorithm for liveness suggested by Howell et al. Lastly, we study structural feature of bounded Petri net where liveness and cs-property are equivalent. From this consideration, liveness problem of bounded normal Petri net is shown to be deterministic polynomial time complexity.

Workflow nets (WF-nets) are Petri nets which represent workflows. Soundness is a criterion of logical correctness defined for WF-nets. It is known that soundness verification is intractable. In this paper, we propose a method to verify soundness using a Linear Temporal Logic (LTL) model checking tool, SPIN. We give an LTL necessary and sufficient condition to verify soundness for WF-nets without livelock. Acyclic WF-nets have no livelock, but cyclic WF-nets may have livelock. We also give a necessary and sufficient condition to verify livelock. Meanwhile, we show that any LTL model checking tool cannot verify soundness for WF-nets with livelock. We give necessary conditions to verify soundness for them. Those conditions enable us to use SPIN even if a given WF-net has livelock. We also develop a tool to verify soundness based on our method. We show effectiveness of our method by comparing our tool with existing soundness verification tools on verification time for 200 cyclic ACWF-nets.

In a Decode and Forward (DF) type of an OFDM-based Full Duplex Relay (FDR), the frequency-domain approach is more efficient than the time-domain approach for feedback interference cancellation. However, Inter-Symbol Interference (ISI) and Inter-Carrier Interference (ICI) may occur due to timing mismatch between the feedback interference signal and the desired signal from the Base Station (BS). In this letter, the effects of a timing mismatch on synchronous types and asynchronous types of OFDM-based FDRs are investigated in uplink and downlink cases. A synchronization procedure and techniques for minimizing ISI and ICI in OFDM-based FDRs with a frequency-domain feedback interference canceller are proposed.

Overlay Access Technology can compensate for the spectrum underutilization problem by exploiting Cognitive Radios capabilities. MAC design is an important aspect of Overlay Access research. In this paper we present the overlay access environment and the challenges it poses to MAC design. Then, we propose the use of a modified Distributed Coordination Function as the MAC protocol for distributed Overlay Access networks. The resulted Intermittent DCF performs with robustness in the demanding overlay access environment, which is characterized by frequent spectrum scan procedure interruptions and low achievable transmission rates. The most recent DCF Markov Chain Model is extended in order to include the overlay operation modifications. Our extension concerns the slot duration expectations calculation which, in the overlay environment, have not constant values but depend on overlay operation parameters. Using the analytical model we evaluate the performance of the DCF under the effect of certain overlay access parameters. The new analytical model predictions are validated with simulations, and are found to accurately capture many interesting features of the overlay operation. Our model can be used in feasibility studies of realistic overlay scenarios and in admission control algorithms of QoS enabled distributed overlay access networks that engage the Intermittent DCF.

High Altitude Platform Stations (HAPS) are recently considered as a green infrastructure to provide high speed multimedia services. The critical issue of HAPS is frequency sharing with satellite systems. Regulating antenna beam pattern using adaptive antenna schemes is one of means to facilitate the sharing with a space receiver for fixed satellite services on the uplink of a HAPS system operating in U bands. In this letter, we investigate antenna beam pattern characteristics of HAPS user terminals with various values of scan angles of main beam, null position angles, and null width.

This paper proposes a frequency asynchronous cross-polarization interference canceller for Vertical/Horizontal (V/H) polarization multiplexing satellite communications. In satellite communications, V/H polarization signals are likely to experience different frequency fluctuations, and so the cross-polarization undergoes two different frequency fluctuations. To cancel this cross-polarization interference, a new frequency asynchronous cross-polarization interference canceller that removes interference and frequency offsets is proposed. Computer simulations are carried out to evaluate its fundamental performance. The results show that the proposed canceller can remove the cross-polarization interference created by the two different frequency offsets, simultaneously.

This paper describes a novel channel allocation scheme that enables data to be collected from observation points throughout the ultra-wide area covered by a satellite communication system. Most of the earth stations in the system acquire pre-scheduled type data such as that pertaining to rainfall and temperature measurements, but a few of them acquire event-driven type data such as that pertaining to earthquakes. Therefore, the main issue pertaining to this scheme is how to effectively accommodate demand for the channels by a huge number of earth stations with limited satellite frequency bandwidth regardless of their acquired data types. To tackle this issue, we propose a channel allocation scheme built on a pre-assigned scheme to gather pre-scheduled type data but that also includes an additional procedure to gather event-driven type data reliably. Performance evaluations show that the proposed scheme achieves higher throughput and lower packet loss rate than conventional schemes.

Current trend in telecommunications is "broadband" and "ubiquitous." To achieve this goal, satellite communications systems are expected to play an important role in cooperation with terrestrial communications systems. Along with the advancement of optical fiber transmission systems, the role of satellite communications was dramatically changed from long distance transmission to various applications utilizing unique features of satellite communications. This paper overviews recent Japanese R&D in satellite communications.

In this paper, we propose a scheme of frequency sub-band allocation to obtain maximum throughput in an orthogonal frequency division multiple access (OFDMA) system where each user has a finite number of packets to transmit, which are generated from packet calls with arbitrary size and arbitrary arrival rate. The proposed scheme is evaluated in terms of throughput and user fairness in comparison with the proportional fairness (PF) scheme and the Greedy scheme under the finite queue length condition. Numerical results show that the proposed scheme is superior to the Greedy scheme in terms of both throughput and fairness for finite queue length.

This paper focuses on fusion estimation algorithms weighted by matrices and scalars, and relationship between them is considered. We present new algorithms that address the computation of matrix weights arising from multidimensional estimation problems. The first algorithm is based on the Cholesky factorization of a cross-covariance block-matrix. This algorithm is equivalent to the standard composite fusion estimation algorithm however it is low-complexity. The second fusion algorithm is based on an approximation scheme which uses special steady-state approximation for local cross-covariances. Such approximation is useful for computing matrix weights in real-time. Subsequent analysis of the proposed fusion algorithms is presented, in which examples demonstrate the low-computational complexity of the new fusion estimation algorithms.

This paper addresses linear quadratic control with state-dependent noise for singularly perturbed stochastic systems (SPSS). First, the asymptotic structure of the stochastic algebraic Riccati equation (SARE) is established for two cases. Second, a new iterative algorithm that combines Newton's method with the fixed point algorithm is established. As a result, the quadratic convergence and the reduced-order computation in the same dimension of the subsystem are attained. As another important feature, a high-order state feedback controller that uses the obtained iterative solution is given and the degradation of the cost performance is investigated for the stochastic case for the first time. Furthermore, the parameter independent controller is also given in case the singular perturbation is unknown. Finally, in order to demonstrate the efficiency of the proposed algorithm, a numerical example is given for the practical megawatt-frequency control problem.

This paper presents a reconfigurable SAD Tree (RSADT) architecture based on adaptive sub-sampling algorithm for HDTV application. Firstly, to obtain the the feature of HDTV picture, pixel difference analysis is applied on each macroblock (MB). Three hardware friendly sub-sampling patterns are selected adaptively to release complexity of homogeneous MB and keep video quality for texture MB. Secondly, since two pipeline stages are inserted, the whole clock speed of RSADT structure is enhanced. Thirdly, to solve data reuse and hardware utilization problem of adaptive algorithm, the RSADT structure adopts pixel data organization in both memory and architecture level, which leads to full data reuse and hardware utilization. Additionally, a cross reuse structure is proposed to efficiently generate 16 pixel scaled configurable SAD (sum of absolute difference). Experimental results show that, our RSADT architecture can averagely save 61.71% processing cycles for integer motion estimation engine and accomplish twice or four times processing capability for homogeneous MBs. The maximum clock frequency of our design is 208 MHz under TSMC 0.18 µm technology in worst work conditions(1.62 V, 125C). Furthermore, the proposed algorithm and reconfigurable structure are favorable to power aware real-time encoding system.

In this paper, we propose a new modeling method to express discrete-time hybrid systems with parameter uncertainty as a mixed logical dynamical (MLD) model. In analysis and control of hybrid systems, there are problem formulations in which convex polyhedra are computed, but for high-dimensional systems, it is difficult to solve these problems within a practical computation time. The key idea of this paper is to use an interval method, which is one of the classical methods in verified numerical computation, and to regard an interval as an over-approximation of a convex polyhedron. By using the obtained MLD model, analysis and synthesis of robust control systems are formulated.

The IEEE 802.16j mobile multi-hop relay (MMR) is studied to improve throughput, extend coverage, and increase capacity. Mobile relay stations attached to vehicles make arbitrary movements and have interference with other base stations or relay stations, thus lowering service functions. This study sets out to suggest an interference detection and avoidance method and evaluates its performance in order to help introduce a mobile relay station for vehicle mounting in a mobile multi-hop relay network. The proposed approach would be implemented by the addition of MAC management messages at a base or relay station instead of the change of mobile station.

Carrier aggregation is a potential technology for the LTE-Advanced system to support wider bandwidth than the LTE system. This paper analyzes the performance of carrier aggregation under elastic traffic, and compares it to that of a simpler approach for the same purpose, referred to as the independent carrier approach. The queueing behaviors of these two approaches are formulated as one fast versus multiple slow state-dependent Processor Sharing servers, respectively. Both analytical and simulation results show that when there are L component carriers with uniform bandwidth in the system, the performance of the carrier aggregation approach is L times better than that of the independent carrier approach in terms of the average user delay and throughput under the same traffic load.

The R&D in satellite communications in Korea has been driven mainly by KCC (Korea Communications Commission) but in a small scale compared to Korea space development program organized by MEST (Ministry of Education, Science and Technology). Public and civilian satcom sector R&D has been led mainly by ETRI with small/medium companies contrary to rare investment in private sector while military sector R&D has been orchestrated by ADD with defense industry. By the COMS (Communication, Ocean and Meteorological Satellite) experimental Ka-band payload, Korea pursues a space qualification of own technology for national infrastructure evolution as well as industrialization of space R&D results. Once COMS launched and space qualified in 2009, subsequent application experiments and new technology R&D like UHDTV will entail service and industry promotion. The payload technology is expected for the next Korean commercial satellites or for new OBP satellites. The COMS ground control system and GNSS ground station technologies are under development for COMS operation and enhanced GNSS services along with advent of Galileo respectively. Satellite broadband mobile VSAT based on DVB-S2/RCS (+M) and low profile tracking antennas have been developed for trains, ships, and planes. While APSI is developing GMR-1 based Thuraya handset functions, ETRI is designing IMT-Advanced satellite radio interface for satellite and terrestrial dual-mode handheld communication system like Japanese STICS, with universities' satellite OFDM researches. A 21 GHz Ka-band higher-availability scalable HD broadcasting technology and SkyLife's hybrid satellite IPTV technology are being developed. In near term Korea will extend R&D programs to upgrade the space communication infrastructure for universal access to digital opportunity and safer daily life from disaster, and to promote space green IT industrialization, national security, and space resources sovereign. Japanese stakeholders are invited to establish a collaborative R&D with Korea for mutual benefit of the future.

This letter proposes a model that allows the effects of hidden terminals on the performance of the S-MAC protocol to be assessed. The model is used to analyze the impact of the number of hidden terminals on the service delay and throughput of the MAC layer. Simulation results show good agreement with our analytical results, which validates the accuracy of our model.

The algebra of communicating shared resources (ACSR) is a timed process algebra which extends classical process algebras with the notion of a resource. In analyzing ACSR models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR, but they are difficult to use for large complex system models in practice. In this paper, we suggest a framework to verify ACSR models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study.

This paper proposes an architecture of an interference canceller for satellite communications with super-posed transmission, which is applicable not only to QPSK but also to 16QAM transmission to get higher satellite capacity. We implement it as an FPGA-based prototype and verify its performance. We propose here to use a new method to measure the satellite round-trip delay using an extended matched filter (EMF), which can work in low C/N conditions such as 0 dB and under. Given this performance, our canceller can work in a network in which forward and reverse links have the same power level. The results of the laboratory tests for QPSK show that interference can be suppressed by about 30 dB and that the BER degradation due to the canceller was small enough for operation.

To realize the harmonious cooperation with the operator, the man-machine cooperative system must be designed so as to accommodate with the characteristics of the operator's skill. One of the important considerations in the skill analysis is to investigate the switching mechanism underlying the skill dynamics. On the other hand, the combination of the feedforward and feedback schemes has been proved to work successfully in the modeling of human skill. In this paper, a new stochastic switched skill model for the sliding task, wherein a minimum jerk motion and feedback schemes are embedded in the different discrete states, is proposed. Then, the parameter estimation algorithm for the proposed switched skill model is derived. Finally, some advantages and applications of the proposed model are discussed.