Probabilistic model checking is an emerging verification technology for probabilistic analysis. Its use has been started not only in computer science but also in interdisciplinary fields. In this paper, we show that probabilistic model checking allows one to analyze the magnetic behaviors of the one-dimensional Ising model, which describes physical phenomena of magnets. The Ising model consists of elementary objects called spins and its dynamics is often represented as the Metropolis method. To analyze the Ising model with probabilistic model checking, we build Discrete Time Markov Chain (DTMC) models that represent the behavior of the Ising model. Two representative physical quantities, i.e., energy and magnetization, are focused on. To assess these quantities using model checking, we devise formulas in Probabilistic real time Computation Tree Logic (PCTL) that represent the quantities. To demonstrate the feasibility of the proposed approach, we show the results of an experiment using the PRISM model checker.

A model that combines free-space loss (proportional to the square of distance d) and excess loss has been known to assess the microwave line-of-sight (LOS) path loss in street microcell environments. The excess loss represents the effects of shadowing obstacles. We measure the path loss at the 3.35, 8.45, and 15.75 GHz frequencies in an urban environment, and analyze the distance characteristics of the pass loss for mobile antenna heights of 2.7, 1.6, and 0.5 m. Results show that using a new model that bases on a dα formula instead of d2 in the conventional model produced a better fit to the measured data. They also show that lowering the mobile antenna to a height of 0. 5 m made it possible to virtually ignore the excess loss factor and, instead, use the dα formula to assess the path loss characteristics.

WiMAX wireless communication has been rapidly developed for broadband mobile communication. Mobile WiMAX communication system uses microwave carrier of 2.5 GHz frequency band and modulation is OFDM mainly. By using OFDM technique, WiMAX provide high speed and reliable communication against multi pass interferences due to the presence of obstacles in communication channels. To design excellent high performance mobile communication systems, accurate evaluation of communication system is indispensable. By using parallel FDTD, we studied fundamental characteristics of microwave propagation and scattering in urban area. We also studied wave propagation and scattering by forest and trees using FDTD method. The effects of multiple scattering and attenuation of microwave by forest are severe factors of high speed wireless communications. In this paper, signal propagation and receiving characteristics of OFDM modulated wave are studied by parallel FDTD method. Propagation, reflection, scattering, interference and delay of digital code signals in received code signals are evaluated to show the environmental characteristics. Parallel FDTD methods are applied for signal and noise analysis about several different complex models and inhomogeneous materials such as forests in long distance communication channels.

Measurements of delay spread were performed at microwave frequencies of 3.35, 8.45 and 15.75 GHz along quasi line-of-sight streets in metropolitan Tokyo. It is found that the delay spreads increase with the measurement distance and reach around 600 ns up to 1 km. It is also confirmed that a cumulative probability of the delay spreads follows a log-normal distribution. The gradients of delay spreads against the distance are greater for a lower mobile antenna height hm = 1.6 m than for hm = 2.7 m in these measurements because of blocking effect by the traffic of vehicles and pedestrians on the road. When the mobile antenna height is 2.7 m, the delay spreads within the range before the break points are observed relatively small: 90 ns (3.35 GHz), 140 ns (8.45 GHz) and 150 ns (15.75 GHz) at the cumulative probability of 90%. The gradients of delay spreads against the distance are greater for wider streets in our measurements.

This paper discusses microwave path-loss characteristics as a function of mobile antenna height in an urban line-of-sight environment. Measurements were made in metropolitan Tokyo with high-density buildings, using base station antenna heights of 4 and 8 m. We describe the path-loss characteristics of vehicle-mounted mode (mobile antenna height is 2.7 m) and portable mode (mobile antenna heights are 1.6 and 0.5 m). Dependence of path loss on the distance between base and mobile stations was analyzed. This reveals that the break points shift to the near side in the vehicle-mounted mode. This phenomenon can be interpreted by the existence of an effective height h of the road. The typical value of h was found approximately 1.4 m. In the portable mode, on the other hand, break points were not observed. The mobile antenna heights (1.6 and 0.5 m) in this mode are close to or less than the average height (1-2 m) of pedestrians on the sidewalk; and the received waves at the mobile station are often disturbed by pedestrians. This explains the nonexistence of break points in portable mode. The average attenuation coefficients is observed 3.2 in this mode. The attenuation coefficients tend to be larger at lower base station antenna heights and narrower road widths.

Properties of Kripke structures can be expressed by formulas of the modal µ-calculus. Despite its strong expressive power, the validity problem of the modal µ-calculus is decidable, and so are some of its variants enriched by inverse programs, graded modalities, and nominals. In this study, we show that the pre- and post-conditions of transformations of Kripke structures, such as addition/deletion of states and edges, can be expressed using variants of the modal µ-calculus. Combined with decision procedures we have developed for those variants, the properties of sequences of transformations on Kripke structures can be deduced. We show that these techniques can be used to verify the properties of pointer-manipulating programs.

This paper describes a method of predicting transmission performance to be obtained by applying RAKE reception and parallel transmission in realistic urban multipath environments. Delay profiles measured in metropolitan Tokyo at microwave frequencies were used to obtain the impulse responses of radio channels, and the closed-form equations corresponding to the performance of these anti-multipath techniques were derived, by means of the characteristic function method, under the assumption that the phases of the impulse responses are uniformly distributed. Results show that RAKE reception provides bit error rates 100 times lower than bare transmission does, whereas the improvement obtained by using parallel transmission should be especially valuable in broadband communication systems, such as those operating at data rates above 10 Mb/s.

There is currently a need for development of a new frequency band to enable creation of next-generation mobile communication systems. Of the potential bands, the 3 GHz and over microwave band holds the greatest promise. Experimental studies on the delay characteristics of multipath propagation must be conducted in order to achieve high-speed transmission in the microwave band. We have developed a system for measuring the microwave broadband propagation delay profile over 100 MHz spread bandwidths in the 3, 8 and 15 GHz bands. Our experiments confirmed system performances of 20-ns resolution, 40-µs maximum measurable delay, relative amplitude error of within 3 dB and dynamic range of over 60 dB. We used our system to measure delay profiles on an urban area with line of sight, particularly, in terms of the effects of mobile antenna height. Typical examples are presented. Analysis showed that delay spreads increased with transmit/receive distance and decreased with the higher antenna height.

Free-space optical communication systems can provide high-speed, improved capacity, cost effective and easy to deploy wireless networks. Experimental investigation on the next generation free-space optical (FSO) communication system utilizing seamless connection of free-space and optical fiber links is presented. A compact antenna which utilizes a miniature fine positioning mirror (FPM) for high-speed beam control and steering is described. The effect of atmospheric turbulence on the beam angle-of-arrival (AOA) fluctuations is shown. The FPM is able to mitigate the power fluctuations at the fiber coupling port caused by this beam angle-of-arrival fluctuations. Experimental results of the FSO system capable of offering stable performance in terms of measured bit-error-rate (BER) showing error free transmission at 2.5 Gbps over extended period of time and improved fiber received power are presented. Also presented are performance results showing stable operation when increasing the FSO communication system data rate from 2.5 Gbps to 10 Gbps as well as WDM experiments.

Probabilistic model checking is an emerging technology for analyzing systems which exhibit stochastic behaviors. The verification of a larger system using probabilistic model checking faces the same state explosion problem as ordinary model checking. Probabilistic symmetry reduction is a technique to tackle this problem. In this paper, we study probabilistic symmetry reduction for a system with a ring buffer which can describe various applications. A key of probabilistic symmetry reduction is identifying symmetry of states with respect to the structure of the target system. We introduce two functions; Shiftδ and Reverse to clarify such symmetry. Using these functions, we also present pseudo code to construct a quotient model. Then, we show two practical case studies; the one-dimensional Ising model and the Automatic Identification System (AIS). Behaviors of them were verified, but suffered from the state explosion problem. Through the case studies, we show that probabilistic symmetry reduction takes advantage of reducing the size of state space.