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.

Voyager Neptune radio science data were collected using three antennas on Earth on August 25, 1989. A parabolic antenna at Canberra, Australia, of 70 meter diameter received 2.3GHz and 8.4GHz carriers. The 64 meter parabolic antennas at Parkes. Australia and Usuda, Japan, received only the 8.4GHz and only the 2.3GHz carriers, respectively. It is necessary to reduce the frequency variation in the received signal carrier to extract accurate information on physically interesting objects such as Neptune's atmosphere, ionosphere, or the rings. After the frequency stabilization process, the frequency drift was reduced from 180Hz down to a maximum of 5Hz, making it possible to reduce the data bandwidth and, consequently, the data volume, by a factor of 30. The uncertainty of the signal frequency estimates were also reduced from 5 down to 510-3Hz/sec above the atmosphere, from 5 down to 0.5Hz/sec in the atmosphere, and from 50 down to 3Hz/sec at the beginning and the end of the atmospheric occultation. Much of the remaining uncertainty is due to scintillations in Neptune's atmosphere and cannot be reduced further. The estimates are thus meaningfully accurate and suitable for scientific analysis and coherent arraying of data from different antennas. Two results based on these estimates are shown: a preliminary temperature-pressure (T-p) profile of Neptune's atmosphere down to a pressure level of 2 bar computed using the Usuda 2.3GHz data, and a multipath phenomenon in the atmosphere seen in Canberra 8.4GHz data. Our T-p profile shows good agreement with the results presented by Lindal et al. within 1K below 100mbar pressure level, even though our result is based on an independent data set and processing. A comparison of the multipath phenomena at Neptune with that at Uranus implies that it was created by a cloud layer with a smaller scale height than the atmosphere above and below it. The processing methods described were developed in part with the interest to coherently array Canberra, Parkes and Usuda data. In this sense, while this paper does not extend any science results, the observations and results are derived independently from other published results, and in the case of Usuda, are completely new.

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.

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.

Unlike a noise removal recursive or averaging filter, this letter presents a temporal filter which attenuates temporal high frequency components and improves visual effects. Although temporal aliasing occurs, the proposed filter proceeds temporal bandlimitation not affected by them. To reduce effects caused by aliasing components, a spatial filtering which is applied along the trajectory of motion is investigated. The proposed filter presents a de-aliasing and effective bandlimiting characteristics as well as reducing of noises.