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

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.
Baldan, Paolo; Corradini, Andrea; Koenig, Barbara; Schwoon, Stefan
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/119050
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 8
social impact