Nonmonotonic reasoning is a logical inference system which attempts to approximate human commonsense reasoning and is characterized as defeasible: having reasonably drawn a conclusion from some premises we may be forced to retract that conclusion upon learning new facts. This paper introduces a Petri net model for nonmonotonic reasoning with nonmonotonic rules generated by annotated logic programs and the unless operator. In the Petri net model, a fixpoint of a nonmonotonic theory can be represented as a maximal and consistent support of a firing sequence. We propose a structural method for finding extensions (coherent consequences) for a given set of nonmonotonic logic rules. It is based on the T-invariant technique for testing fireability of a goal transition in the Petri net model of Horn clause logic programs.

This paper presents an effective application of Net-theory for all the stages of the communication protocol development process. Net-theory provides a basic mathematical model and tool for development of communication protocol. The special usability of Net-theory is that 1) visual representation of the system's stadic/dynamic structure, so that users may easily understand the represented contents, 2) formal specifications based on mathematical basis of Net-theory admit automatic verification, implementation and conformance testing. We have seen that Net-theory which has the above usability can provide a systematic and advanced paradigm for effective communication protocol development.

This paper considers algebraic basic processes, a subset of communicating processes in CCS by Milner, and presents a synthesis algorithm to infer a process that satisfies the properties of the process, represented as fomulae in Hennessy-Milner Logic. The validity of the proposed algorithm can be stated that it synthesizes a process in the limit, which cannot be distinguished from the target one with respect to the strong equivalence.

State space explosion is a serious problem in analyzing discrete event systems that allow concurrent occurring of events. A new method is proposed for generating reduced state spaces of systems. This method is an improvement of Valmari's stubborn set method. The generated state space preserves liveness, livelocks, and terminal states of the ordinary state space. Petri nets are used as a model of systems, and a method is shown for generating a reduced state space from a given Petri net.

This paper presents a novel and successful optimization algorithm for optimizing Multiple-valued Logic (MVL) functions based on Petri net theory. Mathematical properties and Petri net modeling tools to implement MVL systems are introduced. On the basis of these properties and modeling tools, the optimization algorithm can synthesize, analyze and minimize an arbitrary quaternary logic function of n-input variables. The analysis technique of optimization algorithm is a well-established concept from both theories of MVL and Petri nets, and this can be applied to specify and optimize any MVL Petri net system. In this paper, Petri nets of Galois field have been proposed in order to form a complete system, which can be used to realize and construct VLSI circuit of any MVL function. Based on the Petri nets of Galois field and the proposed algorithm, the quaternary minimum and maximum functions have been analyzed, minimized, and designed. These applications have demonstrated the usefulness of optimization algorithm. Based on Petri net theory, the analysis revealed important information about MVL Petri net modeled systems, where this information has been used to evaluate the modeled system and suggest improvements or changes. For evaluation, advantages of the proposed method over a conventional logic minimization method are presented. Also, we have observed that the MVL Petri nets have the following advantages: Designers can exhibit clearly, simply and systematically any complex MVL Petri net nodel, number of concurrent operations is increased, number of places and transitions that are needed to realize a MVL model is very small, and the interconnection problems can be greatly reduced.

Management of control functions in large computer networks is a very difficult problem. One of the effective way to overcome the difficulty is to introduce hierarchical control structure (network cluster) in the management. When a fault occurred in the cluster, routing information at some nodes in the network must be updated in order to react the fault. However, the number of such nodes can be reduced by introducing ingenious topology into the cluster. This paper presents a fundamental discussion on network topology for a network cluster. First, L-FT is defined to represent a degree of fault-tolerance in a cluster with respect to link failures. Secondly, the minimum link problem M is defined to find the minimum number of links to make the cluster L-FT. The following results are obtained. (1) For a network cluster with the fault-tolerant topology 1-FT, at least 2n-2 links have to exist in the cluster where n is the number of border nodes in the cluster. (2) As far as connectivity of the whole network is held, for multiple L link failures in a L-FT cluster, the update of routing information at each node is localized within only the cluster containing the failed links. (3) Several hierarchical networks with fault-tolerant conditions are presented as case studies for a LAN and a MAN.

In a distributed system, the protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events described in a service specification for the distributed system. It is desirable that a correct protocol specification can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes automatically a correct protocol specification from a service specification described as a Marked Graph with Registers (MGR) model and resources (registers and gates) allocation information. This model has a finite control modeled as a marked graph. Therefore, parallel events can be described. In our method, to minimize the number of the exchanged messages, we use a procedure to calculate an optimum solution for 0-1 integer linear programming problems. The number of the steps which each protocol entity needs to simulate one transition in the service specification is also minimized. Ways to avoiding conflict of registers are also described. Our approach has the following advantages. First, parallel events can be described in a service specification. Secondly, many practical systems can be described in the MGR model. Finally, at the protocol specification level, we can understand what events can be executed in parallel.

In the conventional protocol synthesis, it is generally assumed that primitives in service specifications cannot be executed simultaneously at different Service Access Points (SAPs). Thus if some primitives are executed concurrently, then protocol errors of unspecified receptions occur. In this paper, we try to extend a class of service specifications from which protocol specifications are synthesized by the previous methods. We first introduce priorities into primitives in protocol specification so that it always selects exactly one primitive of the highest priority from a set of primitives that can be executed simultaneously, and executes it. Then, based on this execution ordering, we propose a new protocol synthesis method which can avoid protocol errors due to message collisions, communication competitions and so on. By applying the proposed synthesis method, we can automatically synthesize a protocol specifications from a given service specification which includes an arbitraty number of processes and allows parallel execution of primitives.

In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of connunication protocols.

This paper presents a support method for specifying communication systems. Generally, a set of requirements for a target system is partial and ambiguous to construct the whole system, namely it lacks certain necessary descriptions for the target system. To attack this problem, our method enables a designer to obtain such necessary descriptions from specifications stored in a knowledge base, namely by reusing specifications, and helps the designer to specify the target system completely. In our support method, we adopt labelled transition systems (LTSs) which are state transition graphs and are shared as a common notion by most FDTs. Therefore, our method is the common approach to FDTs. We propose a new idea about similarity berween LTSs, and propose an algorithm to suggest similar LTSs to the designer.

As to the method of multi-layer testing, up to now, the testing system (called PROVES) which testes effectively each N-layer protocol implement of SUT (System Under Test) using the functions of derail-points located between N-layer and (N+1)-layer protocol implements in a test system has been proposed. The test logic programs, which are embedded in the derail-points of the test system, play an important role to realize the protocol error test sequences in the test system. Namely, they modify, add, or delete the correct protocol commands/responses output from the protocol implement part of the lest system, sends these erroneous commands/responses to SUT and observes the output from SUT. This paper proposes the method of validating the correctness of test logic program using the structural properties of Petri nets without coding the test logic programs, where correctness means that the desired output can be obtained by sending or receiving the commands/responses within a constant time under the initial conditions determined uniquely by the test system and SUT. According to our experiment, it is seen that almost all of the logical errors included in the test logic programs used for the experiment can be detected by this method.

We present an O(nN) time and O(n²) space algorithm for finding a maximum weight independent set of a circle (or overlap) graph of n chords (or intervals) on N endpoints, based on an alternative definition of such graphs. The results improve on the best previously known algorithms for this case.

Given a sorted set S of n points in the plane, the prefix convex hulls problem of S is to compute the convex hull for every prefix set of S. We present a parallel algorithm for this problem. Our algorithm runs in O(logn) time using n/logn processors in the CREW PRAM computational model. The algorithm is shown to be time and cost optimal. One of the techniques we adopt to achieve these optimal bounds is the use of a new parallel data structure Array-Tree.

This paper describes a preconstrained compaction method and its application to the direct design-rule conversion of CMOS layouts. This approach can convert already designed physical patterns into compacted layouts that satisfy user-specified design rules. Furthermore, preconstrained compaction can eliminate unnecessarily extended diffusion areas and polysilicon wires which tend to be created with conventional longest path based compactions. Preconstrained compaction can be constructed by combining a longest path algorithm with forward and backward slack processes and a preconstraint generation process. This contrasts with previously proposed approaches based on longest path algorithms followed by iterative improvement processes, which include applications of linear programming. The layout styles in those approaches are usually limited to a model where fixed-shaped rectilinear blocks are moved so as to minimize the total length of rectilinear interconnections among the blocks. However, preconstrained compaction can be applied to reshaping polygonal patterns such as diffusion and channel areas. Thus, this compaction method makes it possible to reuse CMOS leaf and macro cell layouts even if design rules change. The proposed preconstrained compaction approach has been applied to direct design-rule conversion from 0.8-µm to 0.5-µm rules of CMOS layouts containing from several to 10,195 transistors. Experimental results demonstrate that a 10.6% reduction in diffusion areas can be achieved without unnecessary extensions of polysilicon wires with a 39% increase in processing times compared with conventional approaches.

A W-graph is a partially known graph which contains wild-components. A wild-component is an incompletely defined connected subgraph having p vertices and p-1 unspecified edges. The informations we know on a wild-component are which has a vertex set and between any two vertices there is one and only one path. In this paper, we discuss the properties of circuits in a W-graph (called W-circuits). Although a W-graph has unspecified edges, we can obtain some important properties of W-circuits. We show that the W-ring sum of W-circuits is also a W-circuit in the same W-graph. The following (1) and (2) are proved: (1) A W-circuit C_i of a W-graph can be transformed into either a circuit or an edge disjoint union of circuits, denoted by C_i^*, of a graph derived from the W-graph, (2) if W-circuits C₁, C₂, ・・・, C_n are linearly independent, then C₁^*, C₂^*, ・・・, C_n^* obtained in (1) are also linearly independent.

A globally and quadratically convergent algorithm is presented for solving nonlinear resistive networks containing transistors modeled by the Gummel-Poon model or the Shichman-Hodges model. This algorithm is based on the Katzenelson algorithm that is globally convergent for a broad class of piecewise-linear resistive networks. An effective restart technique is introduced, by which the algorithm converges to the solutions of the nonlinear resistive networks quadratically. The quadratic convergence is proved and also verified by numerical examples.

It is shown that for a class of interval matrices we can estimate the location of eigenvalues in a very simple way. This class is characterized by the property that eigenvalues of any real linear combination of member matrices are all real and thus includes symmetric interval matrices as a subclass. Upper and lower bounds for each eigenvalue of such a class of interval matrices are provided. This enables us to obtain Hurwitz stability conditions and Schur ones for the class of interval matrices and positive definiteness conditions for symmetric interval matrices.

In the design of 3-D filter detecting Linear Trajectory Signal (LTS), there may be paid little attention to the noise rejective characteristics. In this paper, we treat the noise rejection ability of the filter detecting LTS having margins both in its velocity and direction.

We introduce a procedure to determine the discrete Fourier spectra of the band-limited function from its irregularly distributed samples. The nonuniform data of the signal are represented by the non-orthogonal basis functions (non-harmonic Fourier functions) and discrete Fourier spectra of the signal. We construct a set of orthonormal basis functions from the above mentioned non-orthogonal basis functions using the Gram-Schmidt procedure. Based on the G-S procedure and the property of the orthogonalization, the spectral components of signal can be obtained by the conjugate transpose of orthonormal basis functions, their coefficients matrix and the nonuniform samples. Thus the desired signal can be obtained by the inverse Fourier transform of the determined discrete Fourier spectra. We apply this algorithm to reconstruct a band-limited low-pass and band-pass signal and show that our method provide more stable and better reconstruction than the matrix inversion method.

A technique for pulse code modulation (PCM) encoding using a T-Model neural network is described. Performance evaluation on both the T-Model and the Hopfield model neural-based PCM encoders is carried out with PSpice simulations. The PSpice simulations also show that the T-Model neural-based PCM encoder computes to a global minimum much more effectively and more quickly than the Hopfield one.