Unfolding through processes to compute the complete prefix of Petri nets

The partial-order technique of the unfolding implicitly represents state-space of a Petri net (PN), by in particular preserving the concurrency relations between the events. That makes it possible to contain state-space explosion problem in case of strong concurrency. A complete prefix of unfolding is used to cover all the state-space of a bounded PN: its computation according to the classical approach is based on the concept of adequate order, taking directly into account only safe PN. In this paper, a new approach independent of the concept of adequate order and faithful to the partial-order semantics, consists in creating the events of the unfolding in the context of a single process at the same time. The results of the tests are conclusive for safe and nonsafe PN. Some solutions are presented to improve compactness of the prefix obtained. La technique d'ordre partiel du dépliage représente implicitement l'espace d'état d'un réseau de Petri (RdP), en conservant notamment les relations de concurrence entre les événements. Cela permet de contenir le phénomène de l'explosion combinatoire en cas de forte concurrence. Un préfixe complet de dépliage sert à couvrir tout l'espace d'état d'un RdP borné: son calcul suivant l'approche classique se base sur le concept d'ordre adéquat, ne prenant directement en compte que les RdP saufs. Dans cet article, une nouvelle approche indépendante du concept d'ordre adéquat et fidèle à la sémantique d'ordre partiel, consiste à créer les événements du dépliage dans le contexte d'un unique processus à la fois. Les résultats des tests sont concluants pour les RdP saufs et non saufs. Des solutions sont présentées pour améliorer la compacité du préfixe obtenu.

UNAMBIGUOUS SHARED-MEMORY SYSTEMS

Shared-memory systems appear as a generalization of asynchronous cellular automata. In this paper we relate the partial-order semantics of shared-memory systems to Mazurkiewicz trace languages by means of a new refinement construction. We show that a set of labeled partial orders is recognized by some unambiguous shared-memory system if and only if it is definable in monadic second-order logic and media-bounded.