In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finitestate) Petri nets, which can be used for verification purposes. Contextual nets are a generalisation of Petri nets suited to model systems with readonly access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan’s construction to a suitable encoding of the contextual net into an ordinary net. However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. A construction for generating such a contextual complete prefix has been proposed for a special class of nets, called read-persistent. In this paper, we propose an algorithm that works for arbitrary semi-weighted, bounded contextual nets. The construction explicitly takes into account the fact that, unlike in ordinary or readpersistent nets, an event can have several different histories in general contextual net computations.
McMillan's complete prefix for contextual nets
CORRADINI, ANDREA;
2008-01-01
Abstract
In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finitestate) Petri nets, which can be used for verification purposes. Contextual nets are a generalisation of Petri nets suited to model systems with readonly access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan’s construction to a suitable encoding of the contextual net into an ordinary net. However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. A construction for generating such a contextual complete prefix has been proposed for a special class of nets, called read-persistent. In this paper, we propose an algorithm that works for arbitrary semi-weighted, bounded contextual nets. The construction explicitly takes into account the fact that, unlike in ordinary or readpersistent nets, an event can have several different histories in general contextual net computations.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.