View Related Documents

Abstract

We extend Vautherin's work on behavioural relationships between coloured nets and their skeletons, which are ordinary Petri nets. A desirable property for a coloured net to have is that a marking is dead if and only if the corresponding skeletal marking is dead. This guarantees that for each deadlock (i.e. reachable dead marking) of the coloured net, the corresponding skeletal marking is a deadlock, so coloured deadlocks are lsquopreservedrsquo in the skeleton. Vautherin gave a rather restrictive sufficient condition for the aforementioned property. We formulate two necessary and sufficient conditions, thus identifying the class of coloured nets with lsquodeadlockpreserving skeletonsrsquo. We then show how any coloured net may be lsquorefoldedrsquo to obtain one with the same behaviour as the original and with a deadlock-preserving skeleton. Consequently, all deadlocks of the original net may be detected via this skeleton. Moreover, the refolding transformation is optimal, in the sense that this skeleton is as small as possible.

Fulltext Preview

Image of the first page of the fulltext document