In: W. van der Aalst, J.-M. Colom, F. Kordon, G. Kotsis and D. Moldt (Eds.): Petri Net Approaches for Modelling and Validation, Lincom Studies in Computer Science 01, pages 35-52. Lincom Europa, Munich, 2003, 2003.
Abstract: Signal Transition Graphs (STGs) are net systems with an interpretation, modelling the behaviour of asynchronous digital circuits by sequences of changes of the circuit signals. Although they have become very popular, only restricted syntactical subclasses (free choice nets) are considered in general. Moreover, the analysis techniques applied to these models are essentially based on the state space obtained from the STG, giving rise to the classical state space explosion problem. In this paper we propose a model obtained from the STGs, that is a net system without interpretation. This new model consists of the unterlying net system of the STG plus a set of places representing the values of the circuit signals. Considering this model, we show how general structural analysis techniques can be applied to verify properties of the system, as consistency, CSC or USC. These analysis techniques avoid the construction of the state space. Moreover, we show that with this kind of model of restrictions on the kind of Petri nets to be used are needed.