Tadaaki TANIMOTO Akio NAKATA Hideaki HASHIMOTO Teruo HIGASHINO
In this paper, we propose a parametric model checking algorithm for a subclass of Timed Automata called Parametric Time-Interval Automata (PTIA). In a PTIA, we can specify upper- and lower-bounds of the execution time (time-interval) of each transition using parameter variables. The proposed algorithm takes two inputs, a model described in a PTIA and a property described in a PTIA accepting all invalid infinite/finite runs (called a never claim), or valid finite runs of the model. In the proposed algorithm, firstly we determinize and complement the given property PTIA if it accepts valid finite runs. Secondly, we accelerate the given model, that is, we regard all the actions that are not appeared in the given property PTIA as invisible actions and eliminate them from the model while preserving the set of visible traces and their timings. Thirdly, we construct a parallel composition of the model and the property PTIAs which is accepting all invalid runs that are accepted by the model. Finally, we perform the extension of Double Depth First Search (DDFS), which is used in the automata-theoretic approach to Linear-time Temporal Logic (LTL) model checking, to derive the weakest parameter condition in order that the given model never executes the invalid runs specified by the given property.
Hiroyasu SAKAMOTO Katsuya MATSUMOTO Azusa KUWAHARA Yoshiteru HAYAMI
In this paper, two techniques are proposed for accelerating and stabilizing the Levenberg-Marquardt (LM) method where its conventional stabilizer matrix (identity matrix) is superseded by (1) a diagonal matrix whose elements are column norms of Jacobian matrix J, or (2) a non-diagonal square root matrix of J TJ. Geometrically, these techniques make constraint conditions of the LM method fitted better to relevant cost function than conventional one. Results of numerical simulations show that proposed techniques are effective when both column norm ratio of J and mutual interactions between arguments of the cost function are large. Especially, the technique (2) introduces a new LM method of damped Gauss-Newton (GN) type which satisfies both properties of global convergence and quadratic convergence by controlling Marquardt factor and can stabilize convergence numerically. Performance of the LMM techniques are compared also with a damped GN method with line search procedure.
Shinya MIYAZAKI Mamoru ENDO Masashi YAMADA Junichi HASEGAWA Takami YASUDA Shigeki YOKOI
This paper presents a deformable fast computation elastic model for real-time processing applications. 'Gradational element resolution model' is introduced with fewer elements for fast computation, in which small elements are laid around the object surface and large elements are laid in the center of the object. Elastic element layout is changed dynamically according to the deformation of cutting or tearing objects. The element reconstruction procedure is applied little by little for each step of the recursive motion generation process to avoid an increase in motion computation time.
Haitao LIU Binhong LI Dongsheng QI
A novel parallel acceleration technique is proposed based on intrinsic parallelism characteristics of shooting-and-bouncing ray launching (SBR) algorithm, which has been implemented using the MPI parallel library on common PC cluster instead of dedicated parallel machines. The results reveal that the new technique achieves very large speedup gains and could be the efficient and low-cost propagation prediction solution.
Ye LIU Zheng-Fan LI Mei XUE Rui-Feng XUE
Integral equation method is used to compute three-dimension-structure capacitance in this paper. Since some multi-conductor structures present regular periodic property, the periodic cell is used to reduce the computational domain with adding appropriate magnetic and electric walls. The periodic Green's function in the integral equation method is represented in the form of infinite series with slow convergence. In this paper, Shanks transformation is used to accelerate the convergence. Numerical examples show that the proposed method is accurate with a much higher efficiency in capacitance extraction for 3-D periodic structures.
Hiroki HIGA Ikuo NAKAMURA Nozomu HOSHIMIYA
As one of control command input methods for functional electrical stimulation (FES) system, using the head movements was considered in this paper. In order to detect the head movements, we designed a prototype control command input device using acceleration sensors and verified its validity in experiments. The experimental results showed that the head movements in the lateral flexion and in the flexion/extension were highly detected and separated by the acceleration sensors.
Masataka HASHIRAO Tetsuya KAWASE Iwao SASASE
For radar tracking, the α-β filter and the Kalman filter, both of which do not require large computational requirements, have been widely utilized. However these filters cannot track a maneuvering target accurately. In recent years, the IMM (Interactive Multiple Model) algorithm has been proposed. The IMM is expected to reduce tracking errors for both non-maneuvering and maneuvering target. However, the IMM requires heavy computational burden, because it utilizes multiple Kalman filters in parallel. On the other hand, the α-β filter with an acceleration term which can estimate maneuver acceleration from the past target estimated positions using the kinetic model, has been proposed. This filter is not available for tracking targets under clutter environment, since it does not calculate the covariance matrix which is needed for gate setting. In this paper, we apply the acceleration estimate to the Kalman filter, and propose the hybrid Kalman filter with a constant-velocity filter and an acceleration estimation filter, and it integrates the outputs of two filters using the normalized distance of the prediction error of each filter. The computational requirement of the proposed filter is smaller than that of the IMM since the proposed filter consists of only two Kalman based filters. The proposed method can prevent deteriorating tracking accuracy by reducing the risk of maneuver misdetection when a target maneuvers. We evaluate the performance of the proposed filter by computer simulation, and show the effectiveness of the proposed filter, comparing with the conventional Kalman filter and the two-stage Kalman filter.
On the basis of generalized theory of system design the behavior of the different design trajectories in the design phase space was analyzed. An additional acceleration effect of the design process has been discovered by the analysis of various design strategies with different initial points. This effect can be understood well on the basis of the elaborated design methodology by means of the different design trajectory analysis. This effect is displayed for all analyzed circuits and it reduces additionally the total computer time for the system design.
Antialiased is one of challenging problems to be solved for the high fidelity image synthesis in 3D graphics. In this paper a rasterization processor which is capable of single-pass full-screen antialiasing is presented. To implement a H/W accelerated single-pass antialiased rasterization processor at the reasonable H/W cost and minimized processing performance degradation, our work is mainly focused on the efficient H/W implementation of a modified version of the A-buffer algorithm. For the efficient handling of partial-pixel fragments of the rasterization phase, a new partial-pixel-merging scheme and a simple and efficient new dynamic memory management scheme are proposed. For the final blending of partial-pixels without loss of generality, a parallel subpixel blender is introduced. To study the feasibility of the proposed rasterization processor as a practical rasterization processor, a prototype processor has been designed using a 0.35 µm EML technology. It operates 100 MHz @3.3 V and has the rendering performance from 25M to 80M pixel-fragments/sec depending on the scene complexity.
Barry SHACKLEFORD Etsuko OKUSHI Mitsuhiro YASUDA Hisao KOIZUMI Katsuhiko SEO Hiroto YASUURA
The problem of synthesizing a minimum-cost logic network is formulated for a genetic algorithm (GA). When benchmarked against a commercial logic synthesis tool, an odd parity circuit required 24 basic cells (BCs) versus 28 BCs for the design produced by the commercial system. A magnitude comparator required 20 BCs versus 21 BCs for the commercial system's design. Poor temporal performance, however, is the main disadvantage of the GA-based approach. The design of a hardware-based cost function that would accelerate the GA by several thousand times is described.
This paper proposes two types of acceleration parameters for the Durand-Kerner method and its variant, where the values of parameters are determined at each iteration step. Numerical examples are also shown.
Hideo TATSUNO Yoshio KAJIYAMA Nobuyuki TOKURA
CEFLAR is one way of realizing ATM-ABR with no cell loss. This paper shows that the transition characteristics of CEFLAR(transition time to achieve fair share), important when addressing network fairness, strongly depend on the acceleration-ratio coefficient, not the rate decrease factor or the distance between source and congestion estimation nodes. This paper also shows that the average throughput of a transmission line in transition degrades as the rate decrease factor decreases and as the distance between the source and congestion estimation nodes increases.
Terutaka TAMAI Yasuhiro KURANAGA
Silver is a fundamental material for electrical contact application. In spite of high electrical conductivity and economical advantage, silver surface is corroded easily by environment contained sulfide. A corrosion product as Ag2S deteriorates the property of contact reliability. In order to examine contact reliability, the acceleration tests have been accepted widely in industries. In the present study, the acceleration factor of the contact reliability for the sulfide film on the surface of silver contact which was subject to the tarnish acceleration test was clarified in comparison with the film grown in a normal office environment. The accelerated environment based on the Japan Electric Industry Development Association (JEIDA) standard No.25 was adopted. This environment is consisted of air contained 3 ppm H2S gas under 40, 85-95% RH. The growth rate of the sulfide film (Ag2S) was evaluated by applying the ellipsometry analysis. In the results, it was found that growth of Ag2S film of 500 in thickness in the normal office environment required corrosion time of 3103 h. This thickness of 500 caused increase in contact resistance of 0.1-1.0 (Ω). However, in the accelerated environment, corrosion time decreased to 1.7 h for same thickness. Therefore, the acceleration factor was obtained by comparison of these time as 1.8103 for the standard test of JEIDA.