Up to now, the only useful and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an extended free-choice (EFC) net and its subclasses such as a free-choice (FC) net, a forward conflict free (FCF) net, a marked graph (MG), and a state machine (SM). All the above subclasses are activated only by deadlock-trap properties (i.e., real d-t properties in this paper), which mean that every minimal structural deadlock (MSDL ND=(SD, TD, FD, MoD)) in a net contains at least one live minimal structural trap (MSTR NT=(ST, TT, FT, MoT)) which is initially marked. However, the necessary and sufficient liveness conditions for EFCF, EBCF, EMGEFCFEBCF, AC (EFCFC), and the net with kindling traps NKT have recently been determined, in which each MSDL without real d-t properties was also activated by a new type of trap of trap, i.e., behavioral traps (BTRs), which are defined by introducing a virtual MSTR, a virtual maximal structural trap (virtual STR), a virtual MSDL, and a virtual maximal structural deadlock (virtual SDL) into a target MSDL. In this paper, a structural or initial-marking-based necessary and sufficient condition for local liveness (i.e., virtual deadlock-trap properties) of each MSDL ND s.t. SDST, SDST, SDST (but ND s.t. SDST is dead owing to real deadlock-trap properties) in a general Petri net N is presented by extending that in NKT. Specifically, live minimal behavioral traps (MBTRs) as well as live maximal behavioral traps (BTRs), i.e., virtual deadlock-trap properties, in a general Petri net N are characterized using the real d-t properties of each MSDL ND s.t. SDST for a general Petri net N, which were also obtained by extending the concept of return paths in NKT in connection with an MSDL which contains at least one MSTR and by using the concepts of T-cornucopias and absolute T-cornucopias in a subclass Ñ of N. In other words, BTRs are defined by introducing a virtual MSTR, a virtual STR, a virtual MSDL, and a virtual SDL into a target MSDL without real d-t properties. Additionally, a structural or initial-marking-based necessary and sufficient condition for liveness of a new subclass Nn of a general Petri net N (i.e., a general Petri net without time) is derived, and the usefulness of the obtained results is also discussed.

If a general Petri net N = (S, T, F, Mo) is transition-live under Mo, it is evident that each maximal structural deadlock SDL(D) in N as well as each minimal structural deadlock MSDL (ND) in each D is also transition-live under Mo. However, since the converse of the latter of the above is not always true, it is important to obtain the conditions for this converse to be true if we want to have a useful necessary and sufficient "initial-marking-based" or "structural" liveness condition for N. Up to now, usefull and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an asymmetric choice (AC) net and its subclasses such as an EFC net, an FC net, an FCF net, MG, and SM. However, all the above subclasses are activated only by real or virtual deadlock-trap properties which are local liveness for each minimal deadlocks; in other words, the above topics of this paper are unconditionally satisfied in those subclasses because of their special structure of nets. In this paper, a necessary and sufficient structural liveness condition for a general Petri net N with globally structural live minimal structural deadlocks is presented as follows: The next () or () is satisfied. () N has no SDL D. () If N has at least one SDL D, () or () is satisfied under the condition that each MSDL ND in N is transition-live under Mo. () N has no singular MSDL (α) (i.e., (α-) and (α-)). () If N has at least one singular MSDL (α-)((α-), resp.), every semi-MDSL ()((), resp.) NDS = (SDS, TDS, FDS, MoDS with respect to each singular MSDL (α-)((α-), resp.), is transition-live under the MoDS under the condition of "the condition (**)", where the locally structural liveness for this NDS means (1) or (2)((3), resp.) of Lemma 4-4 and "the condition (**)" is defined in Lemma 4-7 of this paper. The relationship between the above results and the liveness problem for N is also shown.

This paper describes a statistical integration algorithm for color, motion and stereo disparity, and introduces a real-time stereo system that can tell us where and what objects are moving. Regarding the integration algorithm, motion estimation and depth estimation are simultaneously performed by a clustering process based on motion, stereo disparity, color, and pixel position. As a result of the clustering, an image is decomposed into region fragments. Eath fragment is characterized by distribution parameters of spatiotemporal intensity gradients, stereo difference, color and pixel positions. Motion vectors and stereo disparities for each fragment are obtained from those distribution parameters. The real-time stereo system can view the objects with the distribution parameters over frames. The implementation and experiments show that we can utilize the proposed algorithm in real-time applications such as surveillance and human-computer interaction.

Petri nets are useful in modeling and analyzing various types of discrete-event systems such as parallel processing systems, distributed systems, and sequential control systems, because Petri nets can easily be used to represent such properties of these systems as concurrency, nondecidability, and causality. Various behavioral analytic problems on Petri nets are reduced to reachability and liveness on them. It is also known that the decidability of liveness is equivalent to that of reachability which is solvable. However, useful necessary and sufficient structural liveness conditions have been given only for extended free-choice (EFC) nets and their subclasses. Moreover recently, a necessary and sufficient structural liveness condition for a useful subclass NKT=(SKT, TKT, FKT, MoKT) (i.e., a Petri net in which each minimal structural deadlock (MSDL) contains at least one real or virtual kindling trap, each locally structural-live MSDL ND=(SD, TD, FD, MoD) is never globally dead even if all key transitions for local liveness of each MSDL are controlled by the net of SKTSD s.t. SKTSD, and there exists no singular MSDL of type (α)) has also been given. In this paper, in order to give one of the bases for a necessary and sufficient "structural" or "initial-marking-based" liveness condition for a general Petri net N, we will, first, directly present a necessary and sufficient local liveness condition for each MSDL with a real deadlock-trap structure in a subclass Ñ (N) using the net structure and initial token distribution and extending basic concepts used in NKT, where Ñ is a general Petri net without live behavioral traps, local liveness means a useful necessary condition for the above final goal, and real deadlock-trap structure means that each MSDL in Ñ contains at least one minimal structural trap. Secondly, a new subclass is shown in which, if the above locally structural liveness condition for each MSDL holds, then the whole-net liveness is also guaranteed. It is also argued that the obtained results are applicable to describing new live behavioral traps and deriving a necessary and sufficient structural liveness condition, which is the final goal in this work, for a general Petri net N.

This paper proposes a hardware architecture of programmable controller based on Petri nets. The suggested architecture achieves sufficiently rapid processing even as demands on PCs become increasingly more complex. The architecture's speed and efficiency are derived from an automatic and dynamic super scalar computing capability that executes bit instructions and data handling instructions simultaneously without preprocessing, due to the properties of Petri nets. Specific characteristics for both architectural memory-based implementation of Petri nets and evolution algorithms are suggested and classified by the net structure. Analysis of the suggested architectures and effects on performance are also given with mathematical formulas and a computer simulation.

This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.

In this paper, we discuss an abstraction method for Petri nets based on an equivalence of firing sequences of a specified subnet or a specified subset of transitions. Specifically, a method is presented to generate an equivalent net which preserves firing sequences of a specified subnet or a specified subset of transitions. The abstraction can be applied to an efficient behavioral analysis of concurrent systems constructed by composition of modules such as communication networks and Flexible Manufacturing Systems (FMS).

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.

Rewriting logic has been proposed as a unified model of parallel and concurrent computation, especially concurrent object-oriented computation and agent oriented computation. In this paper, we present a category-theoretic technique in which simulation relation between concurrent processes described by rewriting logic is analyzed. In this technique, simulation relation is represented by morphisms in the category of concurrent processes. Moreover, this technique is shown to be applicable to Petri nets by modeling them by rewriting logic. By this method, it is acknowledged that our technique is applicable to Petri nets including multi-loops whose treatment is limited in other techniques.

We present a framework for the unsupervised segmentation of time series. It applies to non-stationary signals originating from different dynamical systems which alternate in time, a phenomenon which appears in many natural systems. In our approach, predictors compete for data points of a given time series. We combine competition and evolutionary inertia to a learning rule. Under this learning rule the system evolves such that the predictors, which finally survive, unambiguously identify the underlying processes. The segmentation achieved by this method is very precise and transients are included, a fact, which makes our approach promising for future applications.

We reported that a competitive learning neural network had the ability of self-organization in the classification of questionnaire survey data. In this letter, its self-organized learning was evaluated by means of mutual information. Mutual information may be useful to find efficently the network which can give optimal classification.

Many typical control problems such as deadlock avoidance problems and mutual exclusion problems can be formulated as forbidden marking problems. This paper studies a forbidden marking problem in controlled complementary-places Petri nets, which are suitable model for sequential control systems. We show a necessary and sufficient condition for the existence of a control law for this problem. We also obtain a maximally permissive control law which allows a maximal number of transitions to fire subject to a condition that forbidden markings will never be reached.

Let L{0,1}* be a language and let λL : {0,1}*{0,1} be the characteristic function of the language L, i.e., if x ∈ L, λL (x) = 1; otherwise,λL (x) = 0. In this paper, we consider an adaptive checker with a single program F (resp. noncommunicating multiple programs F1, F2,...) for λL that works even when an incorrect program F* (resp. incorrect noncommunicating multiple programs F*1,F*2,...) for λL adaptively behaves according to inputs previously provided to the program F* (resp. the programs F*1,F*2,...). We show that (1) for any language L, there exists an adaptive checker with a single program for λL iff L and respectively have competitive interactive proof systems; and (2) that for any language L, there exists an adaptive checker with noncommunicating multiple programs for λL iff L and respectively have function-restricted interactive proof systems. This implies that for any language L, adaptive chekers with noncommunicating multiple programs for λL are as powerful as static ones with a single program for λL.

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.

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.

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.

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.

We study robot navigation in unknown environment with rectangular obstacles aligned with the x and y axes. We propose a strategy called the modified-bian heuristic, and analyze its efficiency. Let n be the distance between the start point and the target of robot navigation, and let k be the maximum side length among the obstacles in a scene. We show that if k=(o(n) and if the summation of the widths of the obstacles on the line crossing the target and along the y axis is o(n), then ratio of the total distance walked by the robot to the shortest path length between the start point and the target is at most arbitrarily close to 1+k/2, as n grows. For the same restrictions as above on the sizes of the obstacles, the ratio is also at most arbitrarily close to 1+3/4n, as n grows, where is the summation of lengths of the obstacles in y axis direction.

Net theory originated by Dr. Petri in 1962 is now indispensable key concept in the analysis and design of concurrent systems. In Japan, since late seventies the net theory has attracted attention among computer scientists. This paper reviews the historical aspect of the net theory developed in Japan during the last two decades.

We consider a class of unknown scenes Sk(n) with rectangular obstacles aligned with the axes such that Euclidean distance between the start point and the target is n, and any side length of each obstacle is at most k. We propose a strategy called the adaptive-bias heuristic for navigating a robot in such a scene, and analyze its efficiency. We show that a ratio of the total distance walked by a robot using the strategy to the shortest path distance between the start point and the target is at most 1+(3/5) k, if k=o(n) and if the start point and the target are at the same horizontal level. This ratio is better than a ratio obtained by any strategy previously known in the class of scenes, Sk(n), such that k=o(n).