McMillan's Complete Prefix for Contextual Nets

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 a new algorithm that works for arbitrary semi-weighted, bounded contextual nets. The construction explicitly takes into account the fact that, unlike ordinar...

• Type: Journal
• Year: 2008
• Where: TOPNOC
• Authors: Paolo Baldan, Andrea Corradini, Barbara König, Stefan Schwoon
• Keywords: Artificial Intelligence, Complete Prefix, Contextual Net, Finite Complete Prefix, TOPNOC 2008