Signal Transition Graphs (STG's) are Petri nets, which were introduced to represent a behavior of asynchronous circuits. To derive logic functions from an STG, the reachability graph should be constructed. In the verification of STG's some method based on an Occurrence net (OCN) and its prefix, called an unfolding, has been proposed. OCN's can represent both causality and concurrency between two nodes by net structure. In this paper, we propose a method to derive a logic function by generating sub state space of a given STG using the structural properties of OCN.

Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.

Signal Transition Graphs (STG'S) [1] are Petrinets [2], which were introduced to represent a behavior of asynchronous circuits. To derive logic functions from an STG, the reachability graph should be constructed. In the verification of STG's some method based on Occurrence nets (OCN) and its prefix, called unfollding, has been proposed [3], [4]. OCN's can represent both causality and concurrency between two nodes by net stryctyre. In this paper, we propose an efficient algorithm to derive a logic function by generating sub-state space of a given STG using the structural properties of OCN. The proposed algorithm can be seem as a parallel algorithm for deriving a logic function.

In this paper, an approach to derive a logic function of asynchronous circuits from a graph-based model called Signal Transition Graphs (STG) is discussed. STG's are Petri nets, whose transitions are interpreted as a signal transition on the circuit inputs or gate outputs, and its marking represents a binary state of the circuit. STG's can represent a behavior of circuit, to derive logic functions, however, the reachability graph should be constructed. In the verification of STG's some method based on Occurrence nets (OCN) and its prefix, called unfolding, has been proposed. OCN's can represent both causality and concurrency between two nodes by net structure. In this paper, we propose a method to derive a logic function by generating substate space of a given STG using the structural properties of OCN. The proposed method can be seem as a parallel algorithm for deriving a logic function.