In this paper we propose a method of formal verfication of fault-tolerance of sequential machines using regular temporal logic. In this method, fault-tolerant properties are described in the form of input-output sequences in regular temporal logic formulas and they are formally verified by checking if they hold for all possible input-output sequences of the machine. We concretely illustrate the method of its application for formal verification of fail-safeness with an example of a comparator for redundant system. The result of verification shows effectiveness of the proposed method.

In this paper, we propose an algorithm of O(|V|min{k,|V|,|A|}|A|) time complexity for finding all k-edge-connected components of a given digraph D=(V,A) and a positive integer k. When D is symmetric, incorporating a preprocessing reduces this time complexity to O(|A|+|V|2+|V|min{k,|V|}min{k|V|,|A|}), which is at most O(|A|+k2|V|2).

In this letter, we propose an algorithm to estimate the optical flow fields based on a hierarchical structure composed of spatio-temporal image pyramids obtained from repetitive application of the Gaussian filtering and decimation in both the spatial and temporal domain. In our approach, an inter-level motion smoothness constraint between adjacent pyramid levels is introduced to estimate a unique optical flow field. We show that the pyramid structure allows us to employ the multigrid algorithm, which is known to accelerate the convergence rate. The multigrid algorithm provides a scheme for efficient combination of local and global information to estimate the optical flow field. The experimental results reveal that the combination of local and global information yields a fast convergence behavior and accurate motion estimation results.

Free choice nets are a class of Petri nets, which can represent the substantial features of systems by modeling both choice and concurrency. And in the modelling and design of a large number of concurrent systems, live and safe free choice nets (LSFC nets) have been explored their structural characteristics. On the other hand, state machine decomposable nets (SMD nets) are a class of Petri nets which can be decomposed by a set of strongly connected state machines (S-decomposition). State machine allocatable nets (SMA nets) are a well-behaved class of SMD nets. Of particular interest is the relation between free choice nets and SMA nets such that a free choice net has a live and safe marking if and only if the net is an SMA net. That is, the structure of an LSFC net is an SMA net. Recently, the structure of SMA net has been completely characterized by the authors based on an S-decomposition. In other words, a necessary and sufficient condition for a net to be an SMA net is obtained in terms of the net structure where synchronization between strongly connected state machine components (S-components) has been clarified. Unfortunately, it requires tremendous amount of time and spaces to decide a given net to be an SMA net by applying the condition directly. Moreover, there exist no efficient algorithm to decide the liveness and safeness of a given SMA net that lessens the usefulness of decomposition techniques. In this paper, we consider efficient polynomial order algorithms to decide whether a given net is a live and safe SHA net.

This paper describes a mixed mode circuit simulation by the direct and relaxation-based methods with dynamic network partitioning. For the efficient circuit simulation by the direct method, the algorithms with circuit partitioning and latency technique have been studied. Recently, the hierarchical decomposition and latency and their validities have been researched. Network tearing techniques enable independent analysis of each subnetwork except for the local datum nodes. Therefore, if the local datum nodes are also torn, each subnetwork is separated entirely. Since the network separation is based on relaxation approach, the implementation of the separation technique in the circuit simulation by the direct method corresponds to performing the mixed mode simulation by the direct and relaxation-based methods. In this paper, a dynamic "network separation" technique based on the tightness of the coupling between subnetworks is suggested. Then, by the introduction of dynamic network separation into the simulator SPLIT with hierarchical decomposition and latency, the mixed mode circuit simulator, which selects the direct method or the relaxation method and determines the block size of the latent circuit dynamically and suitably, is constructed.

Compared to multi-level signature file techniques, PSF (Partitioned Signature File) technique has less processing overhead by its characteristics of a simple file organization. In a multi-processor environment, the PSF technique also has an advantage that queries can be processed in parallel effectively by allocating one or more partitions to each processor. Main point of the PSF technique is a partitioning scheme based on a key selection. In this paper, an n-BFK (n-Bounded Floating Key) partitioning scheme is proposed, in which the number of segments for a key selection is bounded by n. The cost model is developed for the performance evaluation of the proposed scheme. By performance comparison with the existing schemes, the efficiencies of the proposed scheme are shown with respect to a disk access cost, a signature reduction ratio, and an uniformity of workload.

Given an integer N, it is easy to determine whether or not N is prime, because a set of primes is in LPP. Then given a composite number N, is it easy to determine whether or not N is of a specified form? In this paper, we consider a subset of odd composite numbers +1MOD4 (resp. +3MOD4), which is a subset of odd composite numbers consisting of prime factors congruent to 1 (resp. 3) modulo 4, and show that (1) there exists a four move (blackbox simulation) perfect ZKIP for the complement of +1MOD4 without any unproven assumption; (2) there exists a five move (blackbox simulation) perfect ZKIP for +1MOD4 without any unproven assumption; (3) there exists a four move (blackbox simulation) perfect ZKIP for +3MOD4 without any unproven assumption; and (4) there exists a five move (blackbox simulation) statistical ZKIP for the complement of +3MOD4 without any unproven assumption. To the best of our knowledge, these are the first results for a language L that seems to be not random self-reducible but has a constant move blackbox simulation perfect or statistical ZKIP for L and without any unproven assumption.

A new indexing technique for rapid evaluation of nested query on composite object is propoced, reducing the overall cost for retrieval and update. An extended B+ tree is introduced in which object identifier (OID) to be searched and path information usud for update of index record are stored in leaf node and subleaf node, respectively. In this method, the retrieval oeration is applied only for OIDs in the leaf node. The index records of both leaf and subleaf nodes are updated in such a way that the path information in the subleaf node and OIDs in the leaf node are reorganized by deleting and inserting the OIDs. The techniaue presented offers advantages over currently related indexing techniques in data reorganization and index allocation. In the proposed index record, the OIDs to be reorganized are always consecutively provided, and thus only the record directory is updated when an entire page should be removed. In addition, the proposed index can be allocate to a path with the length greater than 3 without splitting the path. Comparisons under a variety of conditions are given with current indexing techniques, showing improved performance in cost, i.e., the total number of pages accessed for retrieval and update.

This paper describes MENDELS ZONE, a Petri-net-based concurrent programming environment, which is especially suitable for cooperating discrete event systems. MENDELS ZONE adopts MENDEL net, which is a type of high level (hierarchical colored) Petri net. One of the characteristics of the MENDEL nets is a process-oriented hierarchy like CCS, which is different from the subnet-oriented hierarchy in the Jensen's hierarchical colored Petri net. In a process-oriented hierarchy, a hierarchical unit is a process, which is more natural for cooperating and decentralized discrete event control systems. This paper also proposes a design methodology for MENDEL nets. Although many Petri net tools have been proposed, most tools support only drawing, simulation, and analysis of Petri nets; few tools support the design methodology for Petri nets. While Petri nets are good final design documents easy to understand, analyzable, and executable it is often difficult to write Petri nets directly in an earlier design phase when the system structure is obscure. A proposed design methodology makes a designer to construct MENDEL nets systematically using causality matrices and temporal logic. Furthemore, constructed MENDEL nets can be automatically compiled into a concurrent programming language and executed on a parallel computer.

This paper surveys modeling techniques for telephone call control based on a Finite State Machine (FSM) concept, and studies model simplification techniques. First, the basic concept and fundamental issues of call control modeling are described. Then, based on the analysis of layered call control configuration, it is clarified that the call control machine decomposition within the two-party service control layer has the effect of reducing the apparent size of each mate's machine. Using this effect, guidelines for call control modeling are derived, by which multiple services can be modeled independently. Finally implementation techniques and a few examples of application will be presented.

Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.

This paper presents a protocol verification method which verifies that the behaviors of a protocol meet requirements. In this method, a protocol specification is expressed as Extended Finite State Machines (EFSM's) that can handle variables, and requirements are expressed using a branching-time temporal logic for a concise and unambiguous description. Using the acyclic expansion algorithm extended such that it can deal with EFSM's, the verification method first generates a state transition graph consisting of executable transitions for each process. Then a branching-time temporal logic formula representing a requirement is evaluated on one of the generated graphs which is relevant to the requirement. An executable state transition graph for each process is much smaller than a global state transition graph which has been used in the conventional verification techniques to represent the behaviors of the whole protocol system consisting of all processes. The computation for generating the graphs is also reduced to much extent for a large complex protocol. As a result, the presented method achieves efficient verification for requirements regarding a state of a process, transmission and reception of messages by a process, varibales of a process and sequences that interact among processes. The validity of the method is illustrated in the paper by the verification of a path-updating protocol for requirements such as process state reachability or fair termination among processes.

Net-Oriented Analysis and Design (NOAD) is defined as three items: (1) Various nets are utilized as an effective modeling method. (2) Inter-relationships among verious nets are determined. (3) Verification or analysis methods for nets are provided and they are implemented based on the mathematical theory, that is Net theory. Very few methods have been presented to satisfy these three items. For example, the Real-Time SA method covers item (1) only. The Object-Oriented Analysis and Design method (OOA/OOD) covers items (1) and (2). NOAD can be regarded as an extension to OOA/OOD. This paper discusses how effectively various nets have been used in actual software development support metnods and tools and evaluates such several methods and tools from the NOAD viewpoint.

We have fabricated superconducting microwave passive components such as resonators, bandpass filters and delay lines with YBCO thin film conductors deposited on MgO substrates. Considerably high unloaded Q values of 12000 at 5.5 GHz was obtained with the YBCO microstrip resonator at 77 K, which indicated that the surface resistance of the YBCO thin film was 0.79 mΩ at that frequency and temperature. Excellent microwave properties were also demonstrated with the bandpass filter and the delay line. Considerably low insertion loss of about 1 dB was obtained with the 10 GHz YBCO bandpass filters at 77 K which have a various bandwidth from 0.5% to 10%. Also excellent microwave propagation was obtained with a 1.3 nsec YBCO coplanar delay line. Its insertion loss was less than 1 dB for the frequencies up to 4 GHz.

This paper describes the properties of non-dispersive and dispersive delay lines fabricated using EuBaCuO superconducting films. The 24 cm long stripline non-dispersive delay line showed a very low loss of 0.3 dB/nsec at 77 K and 10 GHz, and no dispersion at a delay time of 2.3 nsec at frequencies below 20 GHz. The 14 cm long microstrip dispersive delay line with modal dispersion exhibited a relative delay time of approximately 120 psec in the 118 GHz frequency range. The 26 cm long stripline dispersive delay line with structural dispersion due to coupling provided a relative delay time of 230 psec in the above frequency range and roughly the same loss as a non-dispersive delay line.

This paper proposes an efficient design method of three-dimensional (3-D) recursive digital filters for video signal processing via decomposition of magnitude specifications. A given magnitude specification of a 3-D digital filter is decomposed into specifications of 1-D digital filters with three different (horizontal, vertical, and temporal) directions. This decomposition can reduce design problems of 3-D digital filters to design problems of 1-D digital filters, which can be designed with ease by conventional methods. Consequently, design of 3-D digital filters can be efficiently performed without complicated tests for stability and large amount of computations. In order to process video signal in real time, the 1-D digital filters with temporal direction must be causal, which is not the case in horizontal and vertical directions. Since the proposed method can approximate negative magnitude specifications obtained by the decomposition with causal 1-D R filters, the 1-D digital filters with temporal direction can be causal. Therefore the 3-D digital filters designed by the proposed method is suitable for real time video signal processing. The designed 3-D digital filters have a parallel separable structure having high parallelism, regularity and modularity, and thus is suitable for high-speed VLSI implementation.

In this paper, subband image coding with symmetric biorthogonal wavelet filters is studied. In order to implement the symmetric biorthogonal wavelet basis, we use the Laplacian Pyramid Model (LPM) and the trigonometric polynomial solution method. These symmetric biorthogonal wavelet basis are used to form filters in each subband. Also coefficients of the filter are optimized with respect to the coding efficiency. From this optimization, we show that the values of a in the LPM generating kernel have the best coding efficiency in the range of 0.7 to 0.75. We also present an optimal bit allocation method based on considerations of the reconstruction filter characteristics. The step size of each subband uniform quantizer is determined by using this bit allocation method. The coding efficiency of the symmetric biorthogonal wavelet filter is compared with those of other filters: QMF, SSKF and Orthonormal wavelet filter. Simulation results demonstrate that the symmetric biorthogonal wavelet filter is useful as a basic means for image analysis/synthesis filters and can give better coding efficiency than other filters.

In recent years, the digitalization of transmission links, such as optical fibre cables, satellite links, and terrestrial microwave links, has been progressed rapidly in many countries. In addition, many types of digital studio equipment have been developed and TV programs can be produced or edited without any picture quality degradation by using such equipment, for example, digital VTR. A high-efficiency bit-reduction coding system is the most promising and effective means for this situation in terms of reducing the cost of digital transmission of TV programs with high picture quality. Considering this background, a new digital coding system has been developed, which makes it possible to transmit up to 4 NTSC TV programs simultaneously over a single DS3 45Mbps link including two high quality sound channels and one 64kbps ancillary data channel for each TV program. The principal bit-reduction technique employed is 2 dimensional intraframe WHT (Walsh Hadamard Transform) coding, which gives higher coding performance for composite TV signals than DCT (Discrete Cosine Transform) coding. In order to attain high picture quality at around 8Mbps for 4 channel transmission, a 3 dimensional adaptive quantization cube which reflects human visual perception sufficiently is employed in the intraframe WHT coding scheme. The hardware has been made compact like a home use VTR. In this paper, first, the algorithm of the coding scheme developed for the coding system is presented, and then the system configuration and its basic coding performance are described.

A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.

Since Vendler classified aspect into four categories, state, achievement, activity, and accomplishment, much effort has been made to define the notion of aspect logically. It is commonly agreed that aspect represents the general temporal characteristics of events and states. However, there still remains a considerable amount of disagreement about its formal treatment. One of the major problems is that the aspect of a sentence shifts by certain types of sentence construction. For instance, adding time adverbials to a sentence modifies the original aspect, taking the progressive form of the verb changes the aspect, and so on. These phenomena are known as the aspect shifts. The other is the problem known as the imperfective paradox. The imperfective paradox is a problem of the truth definition of the progressives. The truth condition of the progressive form of the sentence is defined at an internal subinterval of the temporal range of the corresponding non-progressive sentence. If the truth condition of the progressive form of the sentence is defined using the truth condition of the non-progressive form of the sentence, there are logical contradictions of truth definition in a sentence such as "Max was building a house, but he never built it". These problems cause much confusion (1) in the truth definition of aspects, (2) in the definition of aspect operations, such as initiative, terminative, progressive, perfective, etc., and also (3) in the definition of adding time adverbials. This paper reviews the semantic problems with respect to aspect, and presents a consistent mechanism of aspect interpretation in order to settle all these semantic puzzles at once. For the sake of logical clarity, we construct a formal language, Lt, where every meaningful formula is a pair of a meaningful sentence and its aspect. The syntax of Lt describes the phenomenology of aspect shifts. The semantics of Lt defines temporal interpretation for all the meaningful sentences of Lt, with assuming the temporal interpretations of three inherent aspects, state, achievement, and activity. The proposed aspect interpretation gives a reasonable account for aspect shifts, and solves the imperfective paradox by asssuming the time structure to be backwards linear.