This paper presents the design and implementation of a hip range of motion (ROM) estimation method that is capable of fine-grained estimation during total hip replacement (THR) surgery. Our method is based on two acceleration strategies: (1) adaptive mesh refinement (AMR) for complexity reduction and (2) parallelization for further acceleration. On the assumption that the hip ROM is a single closed region, the AMR strategy reduces the complexity for N N N stance configurations from O(N3) to O(ND), where 2≤D≤3 and D is a data-dependent value that can be approximated by 2 in most cases. The parallelization strategy employs the master-worker paradigm with multiple task queues, reducing synchronization between processors with load balancing. The experimental results indicate that the implementation on a cluster of 64 PCs completes estimation of 360360180 stance configurations in 20 seconds, playing a key role in selecting and aligning the optimal combination of artificial joint components during THR surgery.

Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.

Video transcoding technique is an efficient mechanism to deliver visual contents to a variety of users who have different network conditions or terminal devices with different display capabilities. In this paper, we propose two types of transcoding methods for adapting the bitrate of streaming video to the bandwidth of the transmission channel; spatial resolution reduction (SRR) transcoding and temporal resolution reduction (TRR) transcoding. The two transcoding methods are alternatively operated according to the requirements of users. Experimental results show that the proposed transcoding methods can preserve image quality while transcoding to the low bitrate.

For producing high quality synthesis, a concatenation-based Text-to-Speech (TTS) system usually requires a large number of segmental units to cover various acoustic-phonetic contexts. However, careful manual labeling and segmentation by human experts, which is still the most reliable way to prepare such units, is labor intensive. In this paper we adopt a two-step procedure to automate the labeling, segmentation and refinement process. In the first step, coarse segmentation of speech data is performed by aligning speech signals with the corresponding sequence of Hidden Markov Models (HMMs). Then in the second step, segment boundaries are refined with a proposed Context-Dependent Boundary Model (CDBM). Classification and Regression Tree (CART) is adopted to organize available data into a structured hierarchical tree, where acoustically similar boundaries are clustered together to train tied CDBM models for boundary refinement. Optimal CDBM parameters and training conditions are found through a series of experimental studies. Comparing with manual segmentation reference, segmentation accuracy (within a tolerance of 20 ms) is improved by the CDBMs from 78.1% (baseline) to 94.8% in Mandarin Chinese and from 81.4% to 92.7% in English, with about 1,000 manually segmented sentences used in training the models. To further reduce the amount of manual data for training CDBMs of a new speaker, we adapt a well-trained CDBM via efficient adaptation algorithms. With only 10-20 manually segmented sentences as adaptation data, the adapted CDBM achieves a segmentation accuracy of 90%.

We present a depth video enhancement algorithm in order to provide high quality haptic interaction. As the telecommunication technology emerges rapidly, the depth image-based haptic interaction is becoming viable for broadcasting applications. Since a real depth map usually contains discrete and rugged noise, its haptic interaction produces the distorted force feedback. To resolve these problems, we propose a two-step refinement and adaptive sampling algorithm. In the first step, noise is removed by the median-filtering technique in 2D image space. Since not all pixels can be used to reconstruct the 3D mesh due to limited system resources, the filtered map is adaptively sampled based on the depth variation. Sampled 2D pixels, called feature points, are triangulated and projected onto 3D space. In the second refinement step, we apply the Gaussian smoothing technique to the reconstructed 3D surface. Finally, 3D surfaces are rendered to compute a smooth depth map from Z-buffer.

We propose a novel approach based on wavelet decomposition for progressive full spectral rendering. In the fourth progressive stage, our method renders an image that is 95% similar to the final non-progressive approach but requires less than 70% of the execution time. The quality of the rendered image is visually plausible that is indistinguishable from that of the non-progressive method. Our approach is graceful, efficient, progressive, and flexible for full spectral rendering.

We introduce an inheritance concept into a specification method of a concurrent system in order to reuse and refine existing specifications. Reusability by inheritance is emphasized in this paper. We take multiple inheritance to enable to reuse several specifications at a time. An upper specification can be skillfully reused by dividing inherited parts and non-inherited ones if the specification contains unnecessary parts for a lower specification. As an application, we specify the FIPA contract net interaction protocol (IP) with the function of an agent authentication. This is accomplished by using multiple inheritance. We also specify the FIPA iterated contract net IP by reusing the FIPA contract net IP. We have been developing a validation support tool for specifications described with the proposed method.

SpecC language is designated to handle the design of entire system from specification to implementation and of hardware/software co-design. Concurrency is one of the features of SpecC which expresses the parallel execution of processes. Describing the systems which contain concurrent behaviors would have some data exchanging or transferring among them. Therefore, the synchronization semantics (notify/wait) of events should be incorporated. The actual design, which is usually sophisticated by its characteristic and functionalities, may contain a bunch of event synchronization codes. This will make the design difficult and time-consuming to verify. In this paper, we introduce a technique which helps verifying the synchronization of events in SpecC. The original SpecC code containing synchronization semantics is parsed and translated into a Boolean SpecC code. The difference decision diagrams (DDDs) is used to verify for event synchronization on Boolean SpecC code. The counter examples for tracing back to the original source are given when the verification results turn out to be unsatisfied. Here we also introduce idea on automatically refinement when the results are unsatisfied and preset some preliminary results.

Machine learning in real-world situations sometimes starts from an initial collection of training instances; learning then proceeds off and on as new training instances come intermittently. The idea of two-phase learning has then been proposed here for effectively solving the learning problems in which training instances come in this two-stage way. Four two-phase learning algorithms based on the learning method PRISM have also been proposed for inducing rules from training instances. These alternatives form a spectrum, showing achievement of the requirement of PRISM (keeping down the number of irrelevant attributes) heavily dependent on the spent computational cost. The suitable alternative, as a trade-off between computational costs and achievement to the requirements, can then be chosen according to the request of the application domains.

In this paper, we propose a descriptor as a shape signature and the projective refinement as a verification method for recognizing 2D curved objects with occlusions from their partial views. For an extracted curve segment, we compute a series of the geometric invariance of equally spaced five co-planar points on the curve. Thus the resulting descriptor is invariant only under rotation, translation, and scale, but sufficient similarity is preserved even under large distortions. It is more stable and robust since it does not need derivatives. We use this transformation-invariant descriptor to index a hash table. We show the efficiency of the method through experiments using seriously distorted images of 2-D curved objects with occlusions.

A new motion field segmentation algorithm under the 8-parameters motion model is presented which uses a multipass iterative region-refining techinique. The iterative region-refining module consists of a seed block detection and subsequent region-refining iterations. An initial estimate of an object motion is provided in the seed block detection process. This initial estimate is iteratively updated and approaches to a reliable mapping parameter set in region-refining process. A multipass composition of the module makes it possible to detect multiple motions in a scene. Our simulation results confirm that the proposed method successfully partitions an image into independently moving objects with allowable computation time.

Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

A stepwise refinement method of communications service specifications is proposed to generate communications software that can conform to any network architecture. This method uses a two-layered language; one layer is a service specification description language (STR), and the other layer is a supplementary specification description language for implementing STR description on a communications system (STR/D). STR specifies terminal behaviors that can be recognized from a perspective outside of the communications systems. With STR, a communications service is defined by a set of rules that can be described without detailed knowledge of communications systems or communications network architectures. Each STR rule describes a global state transition of terminals. Supplementary specifications, such as terminal control and network control, are needed to implement communications services specified by STR rules. These supplementary specifications are described by STR/D rules. Communications services, such as UPT (Universal Personal Telecommunication), are standardized so that they can be provided on a given functional model consisting of functional entities. Specifications for each functional entity in a network are obtained from the two kinds of initially described specifications mentioned above. The obtained specifications are described by STR(L) and STR/D(L) rules, which specify local specifications of a functional entity. These specifications for functional entities are then transformed into software specifications, and finally communications software is generated from these software specifications. This stepwise refinement method makes it possible to generate communications software that can conform to any functional model from service specifications.

In general, the work on developing an expert system has relied on domain experts to provide all domain-specific knowledge. The method for acquiring knowledge directly from experts is inadequate in oriental medicine because it is hard to find an appropriate expert and the development cost becomes too high. Therefore, we have developed two effective methods for acquiring knowledge indirectly from sample cases. One is to refine a constructed knowledge base by using sample cases. The other is to train a neural network by using sample cases. To demonstrate the effectiveness of our methods, we have implemented two prototype systems; the Oriental Medicine Expert System (OMES) and the Oriental Medicine Neural Network (OMNN). These systems have been compared with the system with the knowledge base built directly by domain experts (OLDS). Among these systems, OMES are considered to be superior to other systems in terms of performances, development costs, and practicalness. In this paper, we present our methods, and describe our experimental and comparison results.

This paper presents a system that automatically refines the theory expressed in the function-free first-order logic. Our system can efficiently correct multiple faults in both the concept and subconcepts of the theory, given only the classified examples of the concept. It can refine larger classes of theory than existing systems can since it has overcome many of their limitations. Our system is based on a new combination of an inductive and an explanation-based learning algorithms, which we call the biggest-first multiple-example EBL (BM-EBL). From a learning perspective, our system is an improvement over the FOIL learning system in that our system can accept a theory as well as examples. An experiment shows that when our system is given a theory that has the classification error rate as high as 50%, it can still learn faster and with more accuracy than when it is not given any theory.

This paper attempts to account for intelligibility of practices-based learning (so-called 'learning control') for skill refinement from the viewpoint of Newtonian mechanics. It is shown from an axiomatic approach that an extended notion of passivity for the residual error dynamics of robots plays a crucial role in their ability of learning. More precisely, it is shown that the exponentially weighted passivity with respect to residual velocity vector and torque vector leads the robot system to the convergence of trajectory tracking errors to zero with repeating practices. For a class of tasks when the endpoint is constrained geometrically on a surface, the problem of convergence of residual tracking errors and residual contact-force errors is also discussed on the basis of passivity analysis.