In: Proceedings of the Canadian Conference on Very Large Scale Integration, pages 19-24. November 1993.
Abstract: Nets, process algebras and modal logics are alternative representations of concurrent processes. This work tackles the problem of decomposing a subclass of interpreted Petri nets used in the specification of delay-insensitive interface protocols of VLSI chips called state transition graphs. The decomposition procedure generates a representation of the graph in Milner's Calculus of Communication Systems (CCS) such that the behavioral properties of the protocol are preserved. It is shown that a multi-way synchronization not contemplated in the original CCS is needed to represent AND-causality dependency. The resulting protocol representation in CCS is compositional and amenable to formal methods of verification. For instance, the Edinburgh Concurrency Workbench has been utilized to study the behaviour of protocols which were originally represented by state transition graphs.
Back to the Petri Nets Bibliography